reconsider g = id X as PartFunc of X,X ;
set D = PFuncs (X,X);
defpred S₁[ Element of PFuncs (X,X), Element of PFuncs (X,X), Element of PFuncs (X,X)] means ex f, g being PartFunc of X,X st
( $1 = f & $2 = g & $3 = g (*) f );
A1: for a, b being Element of PFuncs (X,X) ex c being Element of PFuncs (X,X) st S₁[a,b,c]

proof

let a, b be Element of PFuncs (X,X); :: thesis: ex c being Element of PFuncs (X,X) st S₁[a,b,c]
reconsider f = a, g = b as PartFunc of X,X by PARTFUN1:46;
reconsider c = g * f as Element of PFuncs (X,X) by PARTFUN1:45;
take c ; :: thesis: S₁[a,b,c]
take f ; :: thesis: ex g being PartFunc of X,X st
( a = f & b = g & c = g (*) f )
take g ; :: thesis: ( a = f & b = g & c = g (*) f )
thus ( a = f & b = g & c = g (*) f ) ; :: thesis: verum

end;

consider f being BinOp of (PFuncs (X,X)) such that
A2: for a, b being Element of PFuncs (X,X) holds S₁[a,b,f . (a,b)] from BINOP_1:sch 3(A1);
set G = multMagma(# (PFuncs (X,X)),f #);
multMagma(# (PFuncs (X,X)),f #) is constituted-Functions ;
then reconsider G = multMagma(# (PFuncs (X,X)),f #) as strict constituted-Functions multMagma ;
take G ; :: thesis: ( the carrier of G = PFuncs (X,X) & ( for f, g being Element of G holds f [*] g = g (*) f ) )
thus H₁(G) = PFuncs (X,X) ; :: thesis: for f, g being Element of G holds f [*] g = g (*) f
let g, h be Element of G; :: thesis: g [*] h = h (*) g
reconsider g9 = g, h9 = h as Element of PFuncs (X,X) ;
ex g, h being PartFunc of X,X st
( g9 = g & h9 = h & f . (g9,h9) = h (*) g ) by A2;
hence g [*] h = h (*) g ; :: thesis: verum