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:13
.=
((a * b) - (a1 * b)) + ((a1 * b) - (a1 * b1))
by VECTSP_1:11
.=
(((a * b) - (a1 * b)) + (a1 * b)) - (a1 * b1)
by RLVECT_1:28
.=
(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:27
.=
((a - a1) + b) - b1
by RLVECT_1:28
.=
(a - a1) + (b - b1)
by RLVECT_1:28
;
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