defpred S₁[ Element of permutations X, Element of permutations X, set ] means $3 = $2 * $1;
A1: for x, y being Element of permutations X ex z being Element of permutations X st S₁[x,y,z]

proof

let x, y be Element of permutations X; :: thesis: ex z being Element of permutations X st S₁[x,y,z]
reconsider f = x, g = y as Permutation of X by Th1;
g * f in permutations X ;
hence ex z being Element of permutations X st S₁[x,y,z] ; :: thesis: verum

end;

consider F being BinOp of (permutations X) such that
A2: for x, y being Element of permutations X holds S₁[x,y,F . (x,y)] from BINOP_1:sch 3(A1);
set S = multMagma(# (permutations X),F #);
multMagma(# (permutations X),F #) is constituted-Functions ;
then reconsider S = multMagma(# (permutations X),F #) as strict constituted-Functions multMagma ;
take S ; :: thesis: ( the carrier of S = permutations X & ( for x, y being Element of S holds x * y = y * x ) )
thus the carrier of S = permutations X ; :: thesis: for x, y being Element of S holds x * y = y * x
let x, y be Element of S; :: thesis: x * y = y * x
thus x * y = y * x by A2; :: thesis: verum