A1: for p, q, r being Element of (Group_of_Perm n) holds (p * q) * r = p * (q * r)

proof

let p, q, r be Element of (Group_of_Perm n); :: thesis: (p * q) * r = p * (q * r)
reconsider p' = p, q' = q, r' = r as Element of Permutations n by Def13;
A2: ( q' * p' is Permutation of (Seg n) & r' * q' is Permutation of (Seg n) )

proof

reconsider p' = p', q' = q', r' = r' as Permutation of (Seg n) by Def11;
A3: q' * p' is Permutation of (Seg n) ;
r' * q' is Permutation of (Seg n) ;
hence ( q' * p' is Permutation of (Seg n) & r' * q' is Permutation of (Seg n) ) by A3; :: thesis: verum

end;

then A4: q' * p' is Element of Permutations n by Def11;
A5: r' * q' is Element of Permutations n by A2, Def11;
(p * q) * r = the multF of (Group_of_Perm n) . (q' * p'),r' by Def13
.= r' * (q' * p') by A4, Def13
.= (r' * q') * p' by RELAT_1:55
.= the multF of (Group_of_Perm n) . p',(r' * q') by A5, Def13
.= p * (q * r) by Def13 ;
hence (p * q) * r = p * (q * r) ; :: thesis: verum

end;

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 ) )

proof

reconsider e' = idseq n as Element of Permutations n by Def11;
reconsider e = idseq n as Element of (Group_of_Perm n) by Th23;
A6: for p being Element of (Group_of_Perm n) holds
( p * e = p & e * p = p )

proof

let p be Element of (Group_of_Perm n); :: thesis: ( p * e = p & e * p = p )
reconsider p' = p as Element of Permutations n by Def13;
A7: p * e = e' * p' by Def13
.= p by Th24 ;
e * p = p' * e' by Def13
.= p by Th24 ;
hence ( p * e = p & e * p = p ) by A7; :: 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 ) )
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

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 Def13;
reconsider r = q as Permutation of (Seg n) by Def11;
reconsider f = r " as Element of Permutations n by Def11;
reconsider g = f as Element of (Group_of_Perm n) by Th26;
A8: p * g = f * q by Def13
.= e by Th25 ;
A9: g * p = q * f by Def13
.= e by Th25 ;
take g ; :: thesis: ( p * g = e & g * p = e )
thus ( p * g = e & g * p = e ) by A8, A9; :: thesis: verum

end;

hence 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 ) ) by A6; :: thesis: verum

end;

hence ( Group_of_Perm n is associative & Group_of_Perm n is Group-like ) by A1, GROUP_1:5; :: thesis: verum