let n be Nat; :: thesis:
reconsider e = idseq n as Element of by Th23;
reconsider e' = idseq n as Element of Permutations n by Def11;
for p being Element of holds
( p * e = p & e * p = p )

let p be Element of ; :: thesis:
reconsider p' = p as Element of Permutations n by Def13;
A1: e * p = p' * e' by Def13
.= p by Th24 ;
p * e = e' * p' by Def13
.= p by Th24 ;
hence ( p * e = p & e * p = p ) by A1; :: thesis:

end;