theorem :: SETWISEO:36

for X, Y being non empty set
for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds
for Z being non empty set
for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds
for f being Function of X,Y
for g being Function of Y,Z st g . (the_unity_wrt F) = the_unity_wrt G & ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds
for B being Element of Fin X holds g . (F $$ (B,f)) = G $$ (B,(g * f))