let G1, G2 be strict constituted-Functions multMagma ; ( 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
; G1 = G2
set f1 = H2(G1);
set f2 = H2(G2);
now for a, b being Element of G1 holds H2(G1) . (a,b) = H2(G2) . (a,b)let a,
b be
Element of
G1;
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)
;
verum end;
hence
G1 = G2
by A3, A5, BINOP_1:2; verum