set G = GPerms X;
A1: H₁( GFuncs X) = Funcs (X,X) by Def40;
then reconsider f = id X as Element of (GFuncs X) by FUNCT_2:9;
f in H₁( GPerms X) by Def42;
hence GPerms X is unital by Th71; :: thesis: GPerms X is invertible

now :: thesis: for a, b being Element of (GPerms X) ex r, l being Element of (GPerms X) st
( a [*] r = b & l [*] a = b )

reconsider i = f as Element of (GPerms X) by Def42;
let a, b be Element of (GPerms X); :: thesis: ex r, l being Element of (GPerms X) st
( a [*] r = b & l [*] a = b )
H₁( GPerms X) c= H₁( GFuncs X) by Th23;
then reconsider a9 = a, b9 = b as Element of (GFuncs X) ;
reconsider f = a9, g = b9 as Permutation of X by Def42;
A2: ( i = f (*) (f ") & i = (f ") (*) f ) by FUNCT_2:61;
reconsider f9 = f " as Element of (GFuncs X) by A1, FUNCT_2:9;
A3: ( g (*) i = g & i (*) g = g ) by FUNCT_2:17;
reconsider f9 = f9 as Element of (GPerms X) by Def42;
reconsider r = f9 [*] b, l = b [*] f9 as Element of (GPerms X) ;
take r = r; :: thesis: ex l being Element of (GPerms X) st
( a [*] r = b & l [*] a = b )
take l = l; :: thesis: ( a [*] r = b & l [*] a = b )
A4: ( i [*] b = g (*) (id X) & b [*] i = (id X) (*) g ) by Th70;
( a [*] f9 = (f ") (*) f & f9 [*] a = f (*) (f ") ) by Th70;
hence ( a [*] r = b & l [*] a = b ) by A2, A3, A4, Lm1; :: thesis: verum

end;

hence GPerms X is invertible by Th10; :: thesis: verum