let F, G be strict multMagma ; :: thesis: ( the carrier of F = Class (EqRel (X,a)) & ( for x, y being Element of F ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of F . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) & the carrier of G = Class (EqRel (X,a)) & ( for x, y being Element of G ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of G . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) implies F = G )
assume that
A7: the carrier of F = Class (EqRel (X,a)) and
A8: for x, y being Element of F ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of F . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) and
A9: the carrier of G = Class (EqRel (X,a)) and
A10: for x, y being Element of G ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of G . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ; :: thesis: F = G
set g = the multF of G;
set f = the multF of F;
for c, d being Element of F holds the multF of F . (c,d) = the multF of G . (c,d)

proof

let c, d be Element of F; :: thesis: the multF of F . (c,d) = the multF of G . (c,d)
consider P1, Q1 being Loop of a such that
A11: ( c = Class ((EqRel (X,a)),P1) & d = Class ((EqRel (X,a)),Q1) ) and
A12: the multF of F . (c,d) = Class ((EqRel (X,a)),(P1 + Q1)) by A8;
consider P2, Q2 being Loop of a such that
A13: ( c = Class ((EqRel (X,a)),P2) & d = Class ((EqRel (X,a)),Q2) ) and
A14: the multF of G . (c,d) = Class ((EqRel (X,a)),(P2 + Q2)) by A7, A9, A10;
( P1,P2 are_homotopic & Q1,Q2 are_homotopic ) by A11, A13, Th46;
then P1 + Q1,P2 + Q2 are_homotopic by BORSUK_6:75;
hence the multF of F . (c,d) = the multF of G . (c,d) by A12, A14, Th46; :: thesis: verum

end;

hence F = G by A7, A9, BINOP_1:2; :: thesis: verum