A1:
ex e being Element of (Group_of_Perm n) st

for p being Element of (Group_of_Perm n) holds

( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st

( p * g = e & g * p = e ) )

for p being Element of (Group_of_Perm n) holds

( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st

( p * g = e & g * p = e ) )

proof

for p, q, r being Element of (Group_of_Perm n) holds (p * q) * r = p * (q * r)
reconsider e = idseq n as Element of (Group_of_Perm n) by Th5;

take e ; :: thesis: for p being Element of (Group_of_Perm n) holds

( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st

( p * g = e & g * p = e ) )

reconsider e9 = idseq n as Element of Permutations n by Def5;

A2: for p being Element of (Group_of_Perm n) ex g being Element of (Group_of_Perm n) st

( p * g = e & g * p = e )

( p * e = p & e * p = p )

( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st

( p * g = e & g * p = e ) ) by A2; :: thesis: verum

end;take e ; :: thesis: for p being Element of (Group_of_Perm n) holds

( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st

( p * g = e & g * p = e ) )

reconsider e9 = idseq n as Element of Permutations n by Def5;

A2: for p being Element of (Group_of_Perm n) ex g being Element of (Group_of_Perm n) st

( p * g = e & g * p = e )

proof

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

( p * e = p & e * p = p )

proof

hence
for p being Element of (Group_of_Perm n) holds
let p be Element of (Group_of_Perm n); :: 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;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

( p * e = p & e * p = p & ex g being Element of (Group_of_Perm n) st

( p * g = e & g * p = e ) ) by A2; :: thesis: verum

proof

hence
( Group_of_Perm n is associative & Group_of_Perm n is Group-like )
by A1, GROUP_1:1; :: thesis: verum
let p, q, r be Element of (Group_of_Perm n); :: 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) )

A7: r9 * q9 is Element of Permutations n by A5, Def5;

(p * q) * r = the multF of (Group_of_Perm n) . ((q9 * p9),r9) by Def6

.= r9 * (q9 * p9) by A6, Def6

.= (r9 * q9) * p9 by RELAT_1:36

.= the multF of (Group_of_Perm n) . (p9,(r9 * q9)) by A7, Def6

.= p * (q * r) by Def6 ;

hence (p * q) * r = p * (q * r) ; :: thesis: verum

end;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

then A6:
q9 * p9 is Element of Permutations n
by Def5;
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;( 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

A7: r9 * q9 is Element of Permutations n by A5, Def5;

(p * q) * r = the multF of (Group_of_Perm n) . ((q9 * p9),r9) by Def6

.= r9 * (q9 * p9) by A6, Def6

.= (r9 * q9) * p9 by RELAT_1:36

.= the multF of (Group_of_Perm n) . (p9,(r9 * q9)) by A7, Def6

.= p * (q * r) by Def6 ;

hence (p * q) * r = p * (q * r) ; :: thesis: verum