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:

reconsider i = f as Element of (GPerms X) by Def42;
let a, b be Element of (GPerms X); :: thesis:
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:
take l = l; :: thesis:
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:

end;