Funcs (X,X) c= PFuncs (X,X) by FUNCT_2:72;
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 FUNCT_2:66;
x [*] y = g * f by Def37;
hence x [*] y in F by FUNCT_2:9; :: thesis: verum
end;
consider G being non empty strict SubStr of GPFuncs X such that
A2: the carrier of G = F by Lm5, A1;
take G ; :: thesis: the carrier of G = Funcs (X,X)
thus the carrier of G = Funcs (X,X) by A2; :: thesis: verum