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
now :: thesis: for x, y being Element of A holds the multF of A . (x,y) = the multF of B . (x,y)
let 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;
hence A = B by A3, A5, BINOP_1:2; :: thesis: verum