set E = EqRel R,I;
let X, Y be strict doubleLoopStr ; ( the carrier of X = Class (EqRel R,I) & 1. X = Class (EqRel R,I),(1. R) & 0. X = Class (EqRel R,I),(0. R) & ( for x, y being Element of X ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of X . x,y = Class (EqRel R,I),(a + b) ) ) & ( for x, y being Element of X ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of X . x,y = Class (EqRel R,I),(a * b) ) ) & the carrier of Y = Class (EqRel R,I) & 1. Y = Class (EqRel R,I),(1. R) & 0. Y = Class (EqRel R,I),(0. R) & ( for x, y being Element of Y ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of Y . x,y = Class (EqRel R,I),(a + b) ) ) & ( for x, y being Element of Y ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of Y . x,y = Class (EqRel R,I),(a * b) ) ) implies X = Y )
assume that
A13:
the carrier of X = Class (EqRel R,I)
and
A14:
( 1. X = Class (EqRel R,I),(1. R) & 0. X = Class (EqRel R,I),(0. R) )
and
A15:
for x, y being Element of X ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of X . x,y = Class (EqRel R,I),(a + b) )
and
A16:
for x, y being Element of X ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of X . x,y = Class (EqRel R,I),(a * b) )
and
A17:
the carrier of Y = Class (EqRel R,I)
and
A18:
( 1. Y = Class (EqRel R,I),(1. R) & 0. Y = Class (EqRel R,I),(0. R) )
and
A19:
for x, y being Element of Y ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of Y . x,y = Class (EqRel R,I),(a + b) )
and
A20:
for x, y being Element of Y ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of Y . x,y = Class (EqRel R,I),(a * b) )
; X = Y
A21:
for x, y being Element of X holds the multF of X . x,y = the multF of Y . x,y
proof
let x,
y be
Element of
X;
the multF of X . x,y = the multF of Y . x,y
consider a,
b being
Element of
R such that A22:
x = Class (EqRel R,I),
a
and A23:
y = Class (EqRel R,I),
b
and A24:
the
multF of
X . x,
y = Class (EqRel R,I),
(a * b)
by A16;
consider a1,
b1 being
Element of
R such that A25:
x = Class (EqRel R,I),
a1
and A26:
y = Class (EqRel R,I),
b1
and A27:
the
multF of
Y . x,
y = Class (EqRel R,I),
(a1 * b1)
by A13, A17, A20;
b - b1 in I
by A23, A26, Th6;
then A28:
a1 * (b - b1) in I
by IDEAL_1:def 2;
A29:
((a - a1) * b) + (a1 * (b - b1)) =
((a * b) - (a1 * b)) + (a1 * (b - b1))
by VECTSP_1:45
.=
((a * b) - (a1 * b)) + ((a1 * b) - (a1 * b1))
by VECTSP_1:43
.=
(((a * b) - (a1 * b)) + (a1 * b)) - (a1 * b1)
by RLVECT_1:42
.=
(a * b) - (a1 * b1)
by Th1
;
a - a1 in I
by A22, A25, Th6;
then
(a - a1) * b in I
by IDEAL_1:def 3;
then
((a - a1) * b) + (a1 * (b - b1)) in I
by A28, IDEAL_1:def 1;
hence
the
multF of
X . x,
y = the
multF of
Y . x,
y
by A24, A27, A29, Th6;
verum
end;
for x, y being Element of X holds the addF of X . x,y = the addF of Y . x,y
proof
let x,
y be
Element of
X;
the addF of X . x,y = the addF of Y . x,y
consider a,
b being
Element of
R such that A30:
(
x = Class (EqRel R,I),
a &
y = Class (EqRel R,I),
b )
and A31:
the
addF of
X . x,
y = Class (EqRel R,I),
(a + b)
by A15;
consider a1,
b1 being
Element of
R such that A32:
(
x = Class (EqRel R,I),
a1 &
y = Class (EqRel R,I),
b1 )
and A33:
the
addF of
Y . x,
y = Class (EqRel R,I),
(a1 + b1)
by A13, A17, A19;
(
a - a1 in I &
b - b1 in I )
by A30, A32, Th6;
then A34:
(a - a1) + (b - b1) in I
by IDEAL_1:def 1;
(a + b) - (a1 + b1) =
((a + b) - a1) - b1
by RLVECT_1:41
.=
((a - a1) + b) - b1
by RLVECT_1:42
.=
(a - a1) + (b - b1)
by RLVECT_1:42
;
hence
the
addF of
X . x,
y = the
addF of
Y . x,
y
by A31, A33, A34, Th6;
verum
end;
then
the addF of X = the addF of Y
by A13, A17, BINOP_1:2;
hence
X = Y
by A13, A14, A17, A18, A21, BINOP_1:2; verum