let n be Nat; :: thesis:
reconsider e = idseq n as Element of (Group_of_Perm n) by Th11;
reconsider e9 = idseq n as Element of Permutations n by Def12;
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 Def13;
A1: e * p = p9 * e9 by Def13
.= p by Th12 ;
p * e = e9 * p9 by Def13
.= p by Th12 ;
hence ( p * e = p & e * p = p ) by A1; :: thesis:

end;