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 by SubStrEx1, 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;