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

proof

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

end;

A2: H₁( GFuncs X) = Funcs (X,X) by Def40;
then reconsider f = id X as Element of (GFuncs X) by FUNCT_2:12;
A3: 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 = f * g by Th79;
hence S₁[x [*] y] ; :: thesis: verum

end;

consider G being non empty strict SubStr of GFuncs X such that
A4: for f being Element of (GFuncs X) holds
( f in the carrier of G iff S₁[f] ) from MONOID_0:sch 1(A3, A1);
f in H₁(G) by A4;
then reconsider G = G as non empty strict unital SubStr of GFuncs X by Th80;

now

reconsider i = f as Element of G by A4;
let a, b be Element of G; :: thesis: ex r, l being Element of G st
( a [*] r = b & l [*] a = b )
H₁(G) c= H₁( GFuncs X) by Th25;
then reconsider a9 = a, b9 = b as Element of (GFuncs X) by TARSKI:def 3;
reconsider f = a9, g = b9 as Permutation of X by A4;
A5: ( i = f (*) (f ") & i = (f ") (*) f ) by FUNCT_2:88;
reconsider f9 = f " as Element of (GFuncs X) by A2, FUNCT_2:12;
A6: ( g (*) i = g & i (*) g = g ) by FUNCT_2:23;
reconsider f9 = f9 as Element of G by A4;
reconsider r = f9 [*] b, l = b [*] f9 as Element of G ;
take r = r; :: thesis: ex l being Element of G st
( a [*] r = b & l [*] a = b )
take l = l; :: thesis: ( a [*] r = b & l [*] a = b )
A7: ( i [*] b = (id X) (*) g & b [*] i = g (*) (id X) ) by Th79;
( a [*] f9 = f (*) (f ") & f9 [*] a = (f ") (*) f ) by Th79;
hence ( a [*] r = b & l [*] a = b ) by A5, A6, A7, Lm2; :: thesis: verum

end;

then reconsider G = G as non empty strict unital invertible SubStr of GFuncs X by Th12;
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 A4; :: thesis: verum