Funcs X,X c= PFuncs X,X by FUNCT_2:141;
then reconsider F = Funcs X,X as non empty Subset of (GPFuncs X) by Def37;
A1: for x, y being Element of F holds x [*] y in F

proof

let x, y be Element of F; :: thesis: x [*] y in F
reconsider f = x, g = y as Function of X,X by Lm6;
x [*] y = f * g by Def37;
hence x [*] y in F by FUNCT_2:12; :: thesis: verum

end;

consider G being non empty strict SubStr of GPFuncs X such that
A2: the carrier of G = F from MONOID_0:sch 1(A1);
id X in F by FUNCT_2:12;
then reconsider G = G as non empty strict unital SubStr of GPFuncs X by A2, Th80;
take G ; :: thesis: the carrier of G = Funcs X,X
thus the carrier of G = Funcs X,X by A2; :: thesis: verum
consider f being Function of X,X;