let G1, G2 be strict multMagma ; :: thesis: ( the carrier of G1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of G1 . (q,p) = p * q ) & the carrier of G2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of G2 . (q,p) = p * q ) implies G1 = G2 )

assume that

A3: the carrier of G1 = Permutations n and

A4: for q, p being Element of Permutations n holds the multF of G1 . (q,p) = p * q and

A5: the carrier of G2 = Permutations n and

A6: for q, p being Element of Permutations n holds the multF of G2 . (q,p) = p * q ; :: thesis: G1 = G2

assume that

A3: the carrier of G1 = Permutations n and

A4: for q, p being Element of Permutations n holds the multF of G1 . (q,p) = p * q and

A5: the carrier of G2 = Permutations n and

A6: for q, p being Element of Permutations n holds the multF of G2 . (q,p) = p * q ; :: thesis: G1 = G2

now :: thesis: for q, p being Element of G1 holds the multF of G1 . (q,p) = the multF of G2 . (q,p)

hence
G1 = G2
by A3, A5, BINOP_1:2; :: thesis: verumlet q, p be Element of G1; :: thesis: the multF of G1 . (q,p) = the multF of G2 . (q,p)

reconsider q9 = q, p9 = p as Element of Permutations n by A3;

thus the multF of G1 . (q,p) = p9 * q9 by A4

.= the multF of G2 . (q,p) by A6 ; :: thesis: verum

end;reconsider q9 = q, p9 = p as Element of Permutations n by A3;

thus the multF of G1 . (q,p) = p9 * q9 by A4

.= the multF of G2 . (q,p) by A6 ; :: thesis: verum