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;

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 )

hence
1_ (SymGroup X) = id X
by GROUP_1:4; :: thesis: verum( 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;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