defpred S_{1}[ 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_{1}[x,y,z]

A2: for x, y being Element of permutations X holds S_{1}[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

A1: for x, y being Element of permutations X ex z being Element of permutations X st S

proof

consider F being BinOp of (permutations X) such that
let x, y be Element of permutations X; :: thesis: ex z being Element of permutations X st S_{1}[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_{1}[x,y,z]
; :: thesis: verum

end;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

A2: for x, y being Element of permutations X holds S

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