defpred S₁[ Element of (GFuncs X)] means $1 is Permutation of X;
A1: 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;

A2: 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;

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 2(A1, A2);
A4: H₁( GFuncs X) = Funcs X,X by Def40;
then reconsider f = id X as Element of (GFuncs X) by FUNCT_2:12;
f in H₁(G) by A3;
then reconsider G = G as non empty strict unital SubStr of GFuncs X by Th80;

now

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 a' = a, b' = b as Element of (GFuncs X) by TARSKI:def 3;
reconsider i = f as Element of G by A3;
reconsider f = a', g = b' as Permutation of X by A3;
reconsider f' = f " as Element of (GFuncs X) by A4, FUNCT_2:12;
reconsider f' = f' as Element of G by A3;
reconsider r = f' [*] b, l = b [*] f' 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 )
( i = f (*) (f " ) & i = (f " ) (*) f & g (*) i = g & i (*) g = g & a [*] f' = f (*) (f " ) & f' [*] a = (f " ) (*) f & i [*] b = (id X) (*) g & b [*] i = g (*) (id X) ) by Th79, FUNCT_2:23, FUNCT_2:88;
hence ( a [*] r = b & l [*] a = b ) by 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 A3; :: thesis: verum