let X be set ; :: thesis: ( the_unity_wrt the multF of (GPerms X) = id X & 1_ (GPerms X) = id X )
reconsider i = id X as Element of (GPerms X) by Th77;

now :: thesis: for a being Element of (GPerms X) holds
( H₂( GPerms X) . (i,a) = a & H₂( GPerms X) . (a,i) = a )

let a be Element of (GPerms X); :: thesis: ( H₂( GPerms X) . (i,a) = a & H₂( GPerms X) . (a,i) = a )
reconsider f = a as Permutation of X by Th77;
a [*] i = i (*) a by Th70;
then A1: H₂( GPerms X) . (a,i) = i (*) f ;
i [*] a = a (*) i by Th70;
hence ( H₂( GPerms X) . (i,a) = a & H₂( GPerms X) . (a,i) = a ) by A1, FUNCT_2:17; :: thesis: verum

end;

then i is_a_unity_wrt H₂( GPerms X) by BINOP_1:3;
hence the_unity_wrt H₂( GPerms X) = id X by BINOP_1:def 8; :: thesis: 1_ (GPerms X) = id X
hence 1_ (GPerms X) = id X by GROUP_1:22; :: thesis: verum