let F, G be strict multMagma ; ( 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)) )
; 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;
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;
verum
end;
hence
F = G
by A7, A9, BINOP_1:2; verum