Well, how about this, if we use pow4' to be modular exponentiation, i.e. mod15 o pow4? (of course then changing mod15 to take Z -> Z so the types line up) Then

Well, how about this, if we use pow4' to be modular exponentiation, i.e. mod15 o pow4? (of course then changing mod15 to take Z -> Z so the types line up) Then the desired statement showing commutativity is pow4'(mod15(x)) = pow4'(x) = mod15(pow4'(x)) where that last equality is trivial because mod15 o mod15 = mod15 so mod15 o pow4' = mod15 o mod15 o pow4 = mod15 o pow4 = pow4' per associativity of function composition