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 Th86;

now

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 Th86;
a [*] i = a (*) i by Th79;
then A1: H₂( GPerms X) . a,i = f (*) i ;
i [*] a = i (*) a by Th79;
hence ( H₂( GPerms X) . i,a = a & H₂( GPerms X) . a,i = a ) by A1, FUNCT_2:23; :: thesis: verum

end;

then i is_a_unity_wrt H₂( GPerms X) by BINOP_1:11;
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:33; :: thesis: verum