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 f = the multF of F;
set g = the multF of G;
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
and A12:
d = Class (EqRel X,a),
Q1
and A13:
the
multF of
F . c,
d = Class (EqRel X,a),
(P1 + Q1)
by A8;
consider P2,
Q2 being
Loop of
a such that A14:
c = Class (EqRel X,a),
P2
and A15:
d = Class (EqRel X,a),
Q2
and A16:
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, A12, A14, A15, 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 A13, A16, Th47;
:: thesis: verum
end;
hence
F = G
by A7, A9, BINOP_1:2; :: thesis: verum