A1: ex e being Element of () st
for p being Element of () holds
( p * e = p & e * p = p & ex g being Element of () st
( p * g = e & g * p = e ) )
proof
reconsider e = idseq n as Element of () by Th5;
take e ; :: thesis: for p being Element of () holds
( p * e = p & e * p = p & ex g being Element of () st
( p * g = e & g * p = e ) )

reconsider e9 = idseq n as Element of Permutations n by Def5;
A2: for p being Element of () ex g being Element of () st
( p * g = e & g * p = e )
proof
let p be Element of (); :: thesis: ex g being Element of () st
( p * g = e & g * p = e )

reconsider q = p as Element of Permutations n by Def6;
reconsider r = q as Permutation of (Seg n) by Def5;
reconsider f = r " as Element of Permutations n by Def5;
reconsider g = f as Element of () by Th8;
take g ; :: thesis: ( p * g = e & g * p = e )
A3: g * p = q * f by Def6
.= e by Th7 ;
p * g = f * q by Def6
.= e by Th7 ;
hence ( p * g = e & g * p = e ) by A3; :: thesis: verum
end;
for p being Element of () holds
( p * e = p & e * p = p )
proof
let p be Element of (); :: thesis: ( p * e = p & e * p = p )
reconsider p9 = p as Element of Permutations n by Def6;
A4: 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 A4; :: thesis: verum
end;
hence for p being Element of () holds
( p * e = p & e * p = p & ex g being Element of () st
( p * g = e & g * p = e ) ) by A2; :: thesis: verum
end;
for p, q, r being Element of () holds (p * q) * r = p * (q * r)
proof
let p, q, r be Element of (); :: thesis: (p * q) * r = p * (q * r)
reconsider p9 = p, q9 = q, r9 = r as Element of Permutations n by Def6;
A5: ( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) )
proof
reconsider p9 = p9, q9 = q9, r9 = r9 as Permutation of (Seg n) by Def5;
( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) ) ;
hence ( q9 * p9 is Permutation of (Seg n) & r9 * q9 is Permutation of (Seg n) ) ; :: thesis: verum
end;
then A6: q9 * p9 is Element of Permutations n by Def5;
A7: r9 * q9 is Element of Permutations n by ;
(p * q) * r = the multF of () . ((q9 * p9),r9) by Def6
.= r9 * (q9 * p9) by
.= (r9 * q9) * p9 by RELAT_1:36
.= the multF of () . (p9,(r9 * q9)) by
.= p * (q * r) by Def6 ;
hence (p * q) * r = p * (q * r) ; :: thesis: verum
end;
hence ( Group_of_Perm n is associative & Group_of_Perm n is Group-like ) by ; :: thesis: verum