defpred S1[ 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 S1[x,y,z]
proof
let x, y be Element of permutations X; :: thesis: ex z being Element of permutations X st S1[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 S1[x,y,z] ; :: thesis: verum
end;
consider F being BinOp of () such that
A2: for x, y being Element of permutations X holds S1[x,y,F . (x,y)] from set S = multMagma(# (),F #);
multMagma(# (),F #) is constituted-Functions ;
then reconsider S = multMagma(# (),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