let G1, G2 be non empty strict unital associative constituted-Functions multMagma ; :: thesis: ( the carrier of G1 = PFuncs X,X & ( for f, g being Element of G1 holds f [*] g = f (*) g ) & the carrier of G2 = PFuncs X,X & ( for f, g being Element of G2 holds f [*] g = f (*) g ) implies G1 = G2 )
assume that
A5: H₁(G1) = PFuncs X,X and
A6: for f, g being Element of G1 holds f [*] g = f (*) g and
A7: H₁(G2) = PFuncs X,X and
A8: for f, g being Element of G2 holds f [*] g = f (*) g ; :: 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 = a (*) b & a9 [*] b9 = a9 (*) b9 ) 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