defpred S₁[ 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₁[q,p,z]

proof

let q, p be Element of Permutations n; :: thesis: ex z being Element of Permutations n st S₁[q,p,z]
reconsider p = p, q = q as Permutation of (Seg n) by Def12;
reconsider z = p * q as Element of Permutations n by Def12;
take z ; :: thesis: S₁[q,p,z]
thus S₁[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 S₁[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