set SR = Frac S;
set E = EqRel S;
set A = Class (EqRel S);
set SR = Frac S;
let X, Y be strict doubleLoopStr ; ( the carrier of X = Class (EqRel S) & 1. X = Class ((EqRel S),(1. (R,S))) & 0. X = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of X ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of X . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of X ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of X . (x,y) = Class ((EqRel S),(a * b)) ) ) & the carrier of Y = Class (EqRel S) & 1. Y = Class ((EqRel S),(1. (R,S))) & 0. Y = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of Y ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of Y . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of Y ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of Y . (x,y) = Class ((EqRel S),(a * b)) ) ) implies X = Y )
assume that
A13:
the carrier of X = Class (EqRel S)
and
A14:
( 1. X = Class ((EqRel S),(1. (R,S))) & 0. X = Class ((EqRel S),(0. (R,S))) )
and
A15:
for x, y being Element of X ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of X . (x,y) = Class ((EqRel S),(a + b)) )
and
A16:
for x, y being Element of X ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of X . (x,y) = Class ((EqRel S),(a * b)) )
and
A17:
the carrier of Y = Class (EqRel S)
and
A18:
( 1. Y = Class ((EqRel S),(1. (R,S))) & 0. Y = Class ((EqRel S),(0. (R,S))) )
and
A19:
for x, y being Element of Y ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of Y . (x,y) = Class ((EqRel S),(a + b)) )
and
A20:
for x, y being Element of Y ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of Y . (x,y) = Class ((EqRel S),(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
Frac S such that A22:
x = Class (
(EqRel S),
a)
and A23:
y = Class (
(EqRel S),
b)
and A24:
the
multF of
X . (
x,
y)
= Class (
(EqRel S),
(a * b))
by A16;
consider a1,
b1 being
Element of
Frac S such that A25:
x = Class (
(EqRel S),
a1)
and A26:
y = Class (
(EqRel S),
b1)
and A27:
the
multF of
Y . (
x,
y)
= Class (
(EqRel S),
(a1 * b1))
by A13, A17, A20;
A28:
b,
b1 Fr_Eq S
by A23, A26, Th26;
A29:
a,
a1 Fr_Eq S
by A22, A25, Th26;
reconsider u =
a * b as
Element of
Frac S ;
thus
the
multF of
X . (
x,
y)
= the
multF of
Y . (
x,
y)
by A24, A27, Th26, Th27, A28, A29;
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
Frac S such that A30:
(
x = Class (
(EqRel S),
a) &
y = Class (
(EqRel S),
b) )
and A31:
the
addF of
X . (
x,
y)
= Class (
(EqRel S),
(a + b))
by A15;
consider a1,
b1 being
Element of
Frac S such that A32:
(
x = Class (
(EqRel S),
a1) &
y = Class (
(EqRel S),
b1) )
and A33:
the
addF of
Y . (
x,
y)
= Class (
(EqRel S),
(a1 + b1))
by A13, A17, A19;
(
a,
a1 Fr_Eq S &
b,
b1 Fr_Eq S )
by A30, A32, Th26;
hence
the
addF of
X . (
x,
y)
= the
addF of
Y . (
x,
y)
by A31, A33, Th26, Th28;
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