let n be Nat; :: thesis:
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 )

let p be Element of (Group_of_Perm n); :: thesis:
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:

end;