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
A5: H₁(G1) = PFuncs (X,X) and
A6: for f, g being Element of G1 holds f [*] g = g (*) f and
A7: H₁(G2) = PFuncs (X,X) and
A8: for f, g being Element of G2 holds f [*] g = g (*) f ; :: thesis: G1 = G2
set f1 = H₂(G1);
set f2 = H₂(G2);

now

let a, b be Element of G1; :: thesis: H₂(G1) . (a,b) = H₂(G2) . (a,b)
reconsider a9 = a, b9 = b as Element of G2 by A5, A7;
( a [*] b = b (*) a & a9 [*] b9 = b9 (*) a9 ) by A6, A8;
hence H₂(G1) . (a,b) = H₂(G2) . (a,b) ; :: thesis: verum

end;

hence G1 = G2 by A5, A7, BINOP_1:2; :: thesis: verum