deffunc H1( object , object ) -> object = [$2,$1];
let I, J, D be non empty set ; :: thesis: for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let F, G be BinOp of D; :: thesis: for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let f be Function of I,D; :: thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let g be Function of J,D; :: thesis: for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let X be Element of Fin I; :: thesis: for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
let Y be Element of Fin J; :: thesis: ( F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative implies F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) )
assume A1: ( F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) ) ; :: thesis: ( not G is commutative or F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) )
consider h being Function such that
A2: ( dom h = [:J,I:] & ( for x, y being object st x in J & y in I holds
h . (x,y) = H1(x,y) ) ) from FUNCT_3:sch 2();
now :: thesis: for z1, z2 being object st z1 in dom h & z2 in dom h & h . z1 = h . z2 holds
z1 = z2
let z1, z2 be object ; :: thesis: ( z1 in dom h & z2 in dom h & h . z1 = h . z2 implies z1 = z2 )
assume that
A3: z1 in dom h and
A4: z2 in dom h and
A5: h . z1 = h . z2 ; :: thesis: z1 = z2
consider x2, y2 being object such that
A6: z2 = [x2,y2] by A2, A4, RELAT_1:def 1;
( x2 in J & y2 in I ) by A2, A4, A6, ZFMISC_1:87;
then A7: h . (x2,y2) = [y2,x2] by A2;
consider x1, y1 being object such that
A8: z1 = [x1,y1] by A2, A3, RELAT_1:def 1;
( x1 in J & y1 in I ) by A2, A3, A8, ZFMISC_1:87;
then A9: h . (x1,y1) = [y1,x1] by A2;
then y1 = y2 by A5, A8, A6, A7, XTUPLE_0:1;
hence z1 = z2 by A5, A8, A6, A9, A7, XTUPLE_0:1; :: thesis: verum
end;
then A10: h is one-to-one by FUNCT_1:def 4;
A11: for x being object st x in [:J,I:] holds
h . x in [:I,J:]
proof
let x be object ; :: thesis: ( x in [:J,I:] implies h . x in [:I,J:] )
assume A12: x in [:J,I:] ; :: thesis: h . x in [:I,J:]
then consider y, z being object such that
A13: x = [y,z] by RELAT_1:def 1;
A14: ( y in J & z in I ) by A12, A13, ZFMISC_1:87;
then h . (y,z) = [z,y] by A2;
hence h . x in [:I,J:] by A13, A14, ZFMISC_1:87; :: thesis: verum
end;
assume A15: G is commutative ; :: thesis: F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))
A16: G * (g,f) = (G * (f,g)) * h
proof
reconsider G = G as Function of [:D,D:],D ;
A17: dom (G * (g,f)) = [:J,I:] by FUNCT_2:def 1;
A18: dom (G * (f,g)) = [:I,J:] by FUNCT_2:def 1;
A19: for x being object holds
( x in dom (G * (g,f)) iff ( x in dom h & h . x in dom (G * (f,g)) ) )
proof
let x be object ; :: thesis: ( x in dom (G * (g,f)) iff ( x in dom h & h . x in dom (G * (f,g)) ) )
thus ( x in dom (G * (g,f)) implies ( x in dom h & h . x in dom (G * (f,g)) ) ) :: thesis: ( x in dom h & h . x in dom (G * (f,g)) implies x in dom (G * (g,f)) )
proof
assume A20: x in dom (G * (g,f)) ; :: thesis: ( x in dom h & h . x in dom (G * (f,g)) )
then consider y, z being object such that
A21: x = [y,z] by RELAT_1:def 1;
A22: ( y in J & z in I ) by A17, A20, A21, ZFMISC_1:87;
then h . (y,z) = [z,y] by A2;
hence ( x in dom h & h . x in dom (G * (f,g)) ) by A2, A18, A21, A22, ZFMISC_1:87; :: thesis: verum
end;
assume that
A23: x in dom h and
h . x in dom (G * (f,g)) ; :: thesis: x in dom (G * (g,f))
thus x in dom (G * (g,f)) by A2, A23, FUNCT_2:def 1; :: thesis: verum
end;
for x being object st x in dom (G * (g,f)) holds
(G * (g,f)) . x = (G * (f,g)) . (h . x)
proof
let x be object ; :: thesis: ( x in dom (G * (g,f)) implies (G * (g,f)) . x = (G * (f,g)) . (h . x) )
assume A24: x in dom (G * (g,f)) ; :: thesis: (G * (g,f)) . x = (G * (f,g)) . (h . x)
then consider y, z being object such that
A25: x = [y,z] by RELAT_1:def 1;
reconsider z = z as Element of I by A17, A24, A25, ZFMISC_1:87;
reconsider y = y as Element of J by A17, A24, A25, ZFMISC_1:87;
A26: [z,y] in dom (G * (f,g)) by A18, ZFMISC_1:87;
A27: [y,z] in dom (G * (g,f)) by A17, ZFMISC_1:87;
thus (G * (f,g)) . (h . x) = (G * (f,g)) . (h . (y,z)) by A25
.= (G * (f,g)) . (z,y) by A2
.= G . ((f . z),(g . y)) by A26, FINSEQOP:77
.= G . ((g . y),(f . z)) by A15
.= (G * (g,f)) . (y,z) by A27, FINSEQOP:77
.= (G * (g,f)) . x by A25 ; :: thesis: verum
end;
hence G * (g,f) = (G * (f,g)) * h by A19, FUNCT_1:10; :: thesis: verum
end;
A28: ( X c= I & Y c= J ) by FINSUB_1:def 5;
for y being object holds
( y in [:X,Y:] iff y in h .: [:Y,X:] )
proof
let y be object ; :: thesis: ( y in [:X,Y:] iff y in h .: [:Y,X:] )
thus ( y in [:X,Y:] implies y in h .: [:Y,X:] ) :: thesis: ( y in h .: [:Y,X:] implies y in [:X,Y:] )
proof
assume A29: y in [:X,Y:] ; :: thesis: y in h .: [:Y,X:]
then consider y1, x1 being object such that
A30: y = [y1,x1] by RELAT_1:def 1;
A31: ( y1 in X & x1 in Y ) by A29, A30, ZFMISC_1:87;
then A32: ( [x1,y1] in [:Y,X:] & [x1,y1] in dom h ) by A28, A2, ZFMISC_1:87;
h . (x1,y1) = y by A28, A2, A30, A31;
hence y in h .: [:Y,X:] by A32, FUNCT_1:def 6; :: thesis: verum
end;
assume y in h .: [:Y,X:] ; :: thesis: y in [:X,Y:]
then consider x being object such that
x in dom h and
A33: x in [:Y,X:] and
A34: y = h . x by FUNCT_1:def 6;
consider x1, y1 being object such that
A35: x = [x1,y1] by A33, RELAT_1:def 1;
A36: ( x1 in Y & y1 in X ) by A33, A35, ZFMISC_1:87;
y = h . (x1,y1) by A34, A35;
then y = [y1,x1] by A28, A2, A36;
hence y in [:X,Y:] by A36, ZFMISC_1:87; :: thesis: verum
end;
then A37: h .: [:Y,X:] = [:X,Y:] by TARSKI:2;
reconsider h = h as Function of [:J,I:],[:I,J:] by A2, A11, FUNCT_2:3;
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],((G * (f,g)) * h)) by A1, A10, A37, SETWOP_2:6
.= F $$ ([:Y,X:],(G * (g,f))) by A16 ;
hence F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f))) ; :: thesis: verum