defpred S_{1}[ Element of Permutations n, Element of Permutations n, set ] means $3 = $2 * $1;

A1: for q, p being Element of Permutations n ex z being Element of Permutations n st S_{1}[q,p,z]

A2: for q, p being Element of Permutations n holds S_{1}[q,p,o . (q,p)]
from BINOP_1:sch 3(A1);

take multMagma(# (Permutations n),o #) ; :: thesis: ( the carrier of multMagma(# (Permutations n),o #) = Permutations n & ( for q, p being Element of Permutations n holds the multF of multMagma(# (Permutations n),o #) . (q,p) = p * q ) )

thus ( the carrier of multMagma(# (Permutations n),o #) = Permutations n & ( for q, p being Element of Permutations n holds the multF of multMagma(# (Permutations n),o #) . (q,p) = p * q ) ) by A2; :: thesis: verum

A1: for q, p being Element of Permutations n ex z being Element of Permutations n st S

proof

consider o being BinOp of (Permutations n) such that
let q, p be Element of Permutations n; :: thesis: ex z being Element of Permutations n st S_{1}[q,p,z]

reconsider p = p, q = q as Permutation of (Seg n) by Def5;

reconsider z = p * q as Element of Permutations n by Def5;

take z ; :: thesis: S_{1}[q,p,z]

thus S_{1}[q,p,z]
; :: thesis: verum

end;reconsider p = p, q = q as Permutation of (Seg n) by Def5;

reconsider z = p * q as Element of Permutations n by Def5;

take z ; :: thesis: S

thus S

A2: for q, p being Element of Permutations n holds S

take multMagma(# (Permutations n),o #) ; :: thesis: ( the carrier of multMagma(# (Permutations n),o #) = Permutations n & ( for q, p being Element of Permutations n holds the multF of multMagma(# (Permutations n),o #) . (q,p) = p * q ) )

thus ( the carrier of multMagma(# (Permutations n),o #) = Permutations n & ( for q, p being Element of Permutations n holds the multF of multMagma(# (Permutations n),o #) . (q,p) = p * q ) ) by A2; :: thesis: verum