let G1, G2 be strict constituted-Functions multMagma ; :: thesis: ( the carrier of G1 = PFuncs (X,X) & ( for f, g being Element of G1 holds f [*] g = g (*) f ) & the carrier of G2 = PFuncs (X,X) & ( for f, g being Element of G2 holds f [*] g = g (*) f ) implies G1 = G2 )
assume that
A3: H1(G1) = PFuncs (X,X) and
A4: for f, g being Element of G1 holds f [*] g = g (*) f and
A5: H1(G2) = PFuncs (X,X) and
A6: for f, g being Element of G2 holds f [*] g = g (*) f ; :: thesis: G1 = G2
set f1 = H2(G1);
set f2 = H2(G2);
now :: thesis: for a, b being Element of G1 holds H2(G1) . (a,b) = H2(G2) . (a,b)
let a, b be Element of G1; :: thesis: H2(G1) . (a,b) = H2(G2) . (a,b)
reconsider a9 = a, b9 = b as Element of G2 by A3, A5;
( a [*] b = b (*) a & a9 [*] b9 = b9 (*) a9 ) by A4, A6;
hence H2(G1) . (a,b) = H2(G2) . (a,b) ; :: thesis: verum
end;
hence G1 = G2 by A3, A5, BINOP_1:2; :: thesis: verum