let X be set ; :: thesis: 1_ (SymGroup X) = id X
set e = id X;
id X in permutations X ;
then reconsider e = id X as Element of (SymGroup X) by Def2;

now :: thesis: for h being Element of (SymGroup X) holds
( h * e = h & e * h = h )

let h be Element of (SymGroup X); :: thesis: ( h * e = h & e * h = h )
reconsider h1 = h as Permutation of X by Th5;
thus h * e = e * h1 by Def2
.= h by FUNCT_2:17 ; :: thesis: e * h = h
thus e * h = h1 * e by Def2
.= h by FUNCT_2:17 ; :: thesis: verum

end;

hence 1_ (SymGroup X) = id X by GROUP_1:4; :: thesis: verum