let X, Y be non empty set ; :: thesis: 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)
let F be BinOp of Y; :: thesis: ( F is commutative & F is associative & F is idempotent & F is having_a_unity implies 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) )
assume that
A1: ( F is commutative & F is associative ) and
A2: F is idempotent and
A3: F is having_a_unity ; :: thesis: 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)
let Z be non empty set ; :: thesis: 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)
let G be BinOp of Z; :: thesis: ( G is commutative & G is associative & G is idempotent & G is having_a_unity implies 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) )
assume that
A4: ( G is commutative & G is associative ) and
A5: G is idempotent and
A6: G is having_a_unity ; :: thesis: 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)
let f be Function of X,Y; :: thesis: 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)
let g be Function of Y,Z; :: thesis: ( 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) ) implies for B being Element of Fin X holds g . (F $$ B,f) = G $$ B,(g * f) )
assume that
A7: g . (the_unity_wrt F) = the_unity_wrt G and
A8: for x, y being Element of Y holds g . (F . x,y) = G . (g . x),(g . y) ; :: thesis: for B being Element of Fin X holds g . (F $$ B,f) = G $$ B,(g * f)
let B be Element of Fin X; :: thesis: g . (F $$ B,f) = G $$ B,(g * f)

per cases ( B = {} or B <> {} ) ;

suppose B = {} ; :: thesis: g . (F $$ B,f) = G $$ B,(g * f)

then A9: B = {}. X ;
hence g . (F $$ B,f) = g . (the_unity_wrt F) by A1, A3, Th40
.= G $$ B,(g * f) by A4, A6, A7, A9, Th40 ;
:: thesis: verum

end;

suppose B <> {} ; :: thesis: g . (F $$ B,f) = G $$ B,(g * f)

hence g . (F $$ B,f) = G $$ B,(g * f) by A1, A2, A4, A5, A8, Th39; :: thesis: verum

end;

end;