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, Th47;
then
P1 + Q1,
P2 + Q2 are_homotopic
by BORSUK_6:83;
hence
the
multF of
F . c,
d = the
multF of
G . c,
d
by A12, A14, Th47;
verum
end;
hence
F = G
by A7, A9, BINOP_1:2; verum