defpred S₁[ Element of (GFuncs X)] means $1 is Permutation of X;
A1: ex x being Element of (GFuncs X) st S₁[x]

proof

set f = the Permutation of X;
H₁( GFuncs X) = Funcs (X,X) by Def40;
then reconsider x = the Permutation of X as Element of (GFuncs X) by FUNCT_2:9;
take x ; :: thesis: S₁[x]
thus S₁[x] ; :: thesis: verum

end;

H₁( GFuncs X) = Funcs (X,X) by Def40;
then reconsider f = id X as Element of (GFuncs X) by FUNCT_2:9;
A2: for x, y being Element of (GFuncs X) st S₁[x] & S₁[y] holds
S₁[x [*] y]

proof

let x, y be Element of (GFuncs X); :: thesis: ( S₁[x] & S₁[y] implies S₁[x [*] y] )
assume ( x is Permutation of X & y is Permutation of X ) ; :: thesis: S₁[x [*] y]
then reconsider f = x, g = y as Permutation of X ;
x [*] y = g * f by Th70;
hence S₁[x [*] y] ; :: thesis: verum

end;

consider G being non empty strict SubStr of GFuncs X such that
A3: for f being Element of (GFuncs X) holds
( f in the carrier of G iff S₁[f] ) from MONOID_0:sch 1(A2, A1);
take G ; :: thesis: for f being Element of (GFuncs X) holds
( f in the carrier of G iff f is Permutation of X )
thus for f being Element of (GFuncs X) holds
( f in the carrier of G iff f is Permutation of X ) by A3; :: thesis: verum