let n be Nat; :: thesis:
reconsider e = idseq n as Element of (Group_of_Perm n) by Th20;
reconsider e9 = idseq n as Element of Permutations n by Def9;
for p being Element of (Group_of_Perm n) holds
( p * e = p & e * p = p )

let p be Element of (Group_of_Perm n); :: thesis:
reconsider p9 = p as Element of Permutations n by Def10;
A1: e * p = p9 * e9 by Def10
.= p by Th21 ;
p * e = e9 * p9 by Def10
.= p by Th21 ;
hence ( p * e = p & e * p = p ) by A1; :: thesis:

end;