let n be Nat; :: thesis: idseq n = 1_ (Group_of_Perm n)

reconsider e = idseq n as Element of (Group_of_Perm n) by Th5;

reconsider e9 = idseq n as Element of Permutations n by Def5;

for p being Element of (Group_of_Perm n) holds

( p * e = p & e * p = p )

reconsider e = idseq n as Element of (Group_of_Perm n) by Th5;

reconsider e9 = idseq n as Element of Permutations n by Def5;

for p being Element of (Group_of_Perm n) holds

( p * e = p & e * p = p )

proof

hence
idseq n = 1_ (Group_of_Perm n)
by GROUP_1:4; :: thesis: verum
let p be Element of (Group_of_Perm n); :: thesis: ( p * e = p & e * p = p )

reconsider p9 = p as Element of Permutations n by Def6;

A1: e * p = p9 * e9 by Def6

.= p by Th6 ;

p * e = e9 * p9 by Def6

.= p by Th6 ;

hence ( p * e = p & e * p = p ) by A1; :: thesis: verum

end;reconsider p9 = p as Element of Permutations n by Def6;

A1: e * p = p9 * e9 by Def6

.= p by Th6 ;

p * e = e9 * p9 by Def6

.= p by Th6 ;

hence ( p * e = p & e * p = p ) by A1; :: thesis: verum