let A, B be strict constituted-Functions multMagma ; :: thesis: ( the carrier of A = permutations X & ( for x, y being Element of A holds x * y = y * x ) & the carrier of B = permutations X & ( for x, y being Element of B holds x * y = y * x ) implies A = B )

assume that

A3: the carrier of A = permutations X and

A4: for x, y being Element of A holds x * y = y * x and

A5: the carrier of B = permutations X and

A6: for x, y being Element of B holds x * y = y * x ; :: thesis: A = B

assume that

A3: the carrier of A = permutations X and

A4: for x, y being Element of A holds x * y = y * x and

A5: the carrier of B = permutations X and

A6: for x, y being Element of B holds x * y = y * x ; :: thesis: A = B

now :: thesis: for x, y being Element of A holds the multF of A . (x,y) = the multF of B . (x,y)

hence
A = B
by A3, A5, BINOP_1:2; :: thesis: verumlet x, y be Element of A; :: thesis: the multF of A . (x,y) = the multF of B . (x,y)

reconsider f = x, g = y as Element of B by A3, A5;

thus the multF of A . (x,y) = x * y

.= y * x by A4

.= f * g by A6

.= the multF of B . (x,y) ; :: thesis: verum

end;reconsider f = x, g = y as Element of B by A3, A5;

thus the multF of A . (x,y) = x * y

.= y * x by A4

.= f * g by A6

.= the multF of B . (x,y) ; :: thesis: verum