defpred S1[ 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 S1[q,p,z]
proof
let q, p be Element of Permutations n; :: thesis: ex z being Element of Permutations n st S1[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: S1[q,p,z]
thus S1[q,p,z] ; :: thesis: verum
end;
consider o being BinOp of (Permutations n) such that
A2: for q, p being Element of Permutations n holds S1[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