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

now

let q, p be Element of G1; :: thesis: the multF of G1 . q,p = the multF of G2 . q,p
reconsider q' = q, p' = p as Element of Permutations n by A3;
thus the multF of G1 . q,p = p' * q' by A4
.= the multF of G2 . q,p by A6 ; :: thesis: verum

end;

hence G1 = G2 by A3, A5, BINOP_1:2; :: thesis: verum