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 = f (*) g );
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:120;
reconsider c = f * g as Element of PFuncs X,X by PARTFUN1:119;
take c ; :: thesis: S₁[a,b,c]
take f ; :: thesis: ex g being PartFunc of X,X st
( a = f & b = g & c = f (*) g )
take g ; :: thesis: ( a = f & b = g & c = f (*) g )
thus ( a = f & b = g & c = f (*) g ) ; :: 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

proof

let x be Element of multMagma(# (PFuncs X,X),f #); :: according to MONOID_0:def 1 :: thesis: x is Function
thus x is Function by PARTFUN1:120; :: thesis: verum

end;

then reconsider G = multMagma(# (PFuncs X,X),f #) as non empty strict constituted-Functions multMagma ;

A3: now

let a, b be Element of G; :: thesis: a [*] b = a (*) b
consider g, h being PartFunc of X,X such that
A4: ( a = g & b = h & f . a,b = g (*) h ) by A2;
thus a [*] b = a (*) b by A4; :: thesis: verum

end;

reconsider g = id X as PartFunc of X,X ;
reconsider f1 = g as Element of G by PARTFUN1:119;

A5: now

let h be Element of G; :: thesis: ( f1 [*] h = h & h [*] f1 = h )
reconsider j = h as PartFunc of X,X by PARTFUN1:120;
thus f1 [*] h = g (*) j by A3
.= h by PARTFUN1:37 ; :: thesis: h [*] f1 = h
thus h [*] f1 = j (*) g by A3
.= h by PARTFUN1:36 ; :: thesis: verum

end;

now

let f', g, h be Element of G; :: thesis: (f' [*] g) [*] h = f' [*] (g [*] h)
reconsider fg = f' [*] g, gh = g [*] h as Element of G ;
thus (f' [*] g) [*] h = fg (*) h by A3
.= (f' (*) g) (*) h by A3
.= f' (*) (g (*) h) by RELAT_1:55
.= f' (*) gh by A3
.= f' [*] (g [*] h) by A3 ; :: thesis: verum

end;

then reconsider G = G as non empty strict unital associative constituted-Functions multMagma by A5, Lm2, Th6;
take G ; :: thesis: ( the carrier of G = PFuncs X,X & ( for f, g being Element of G holds f [*] g = f (*) g ) )
thus H₁(G) = PFuncs X,X ; :: thesis: for f, g being Element of G holds f [*] g = f (*) g
let g, h be Element of G; :: thesis: g [*] h = g (*) h
reconsider g' = g, h' = h as Element of PFuncs X,X ;
( f . g,h = g [*] h & ex g, h being PartFunc of X,X st
( g' = g & h' = h & f . g',h' = g (*) h ) ) by A2;
hence g [*] h = g (*) h ; :: thesis: verum