set E = EqRel S;
set A = Class (EqRel S);
set SR = Frac S;
defpred S1[ set , set , set ] means ex P, Q being Element of Frac S st
( $1 = Class ((EqRel S),P) & $2 = Class ((EqRel S),Q) & $3 = Class ((EqRel S),(P + Q)) );
defpred S2[ set , set , set ] means ex P, Q being Element of Frac S st
( $1 = Class ((EqRel S),P) & $2 = Class ((EqRel S),Q) & $3 = Class ((EqRel S),(P * Q)) );
reconsider u = Class ((EqRel S),(1. (R,S))) as Element of Class (EqRel S) by EQREL_1:def 3;
reconsider z = Class ((EqRel S),(0. (R,S))) as Element of Class (EqRel S) by EQREL_1:def 3;
A1:
for x, y being Element of Class (EqRel S) ex z being Element of Class (EqRel S) st S1[x,y,z]
proof
let x,
y be
Element of
Class (EqRel S);
ex z being Element of Class (EqRel S) st S1[x,y,z]
consider P being
object such that A2:
P in Frac S
and A3:
x = Class (
(EqRel S),
P)
by EQREL_1:def 3;
consider Q being
object such that A4:
Q in Frac S
and A5:
y = Class (
(EqRel S),
Q)
by EQREL_1:def 3;
reconsider P =
P,
Q =
Q as
Element of
Frac S by A2, A4;
Class (
(EqRel S),
(P + Q)) is
Element of
Class (EqRel S)
by EQREL_1:def 3;
hence
ex
z being
Element of
Class (EqRel S) st
S1[
x,
y,
z]
by A3, A5;
verum
end;
consider g being BinOp of (Class (EqRel S)) such that
A6:
for a, b being Element of Class (EqRel S) holds S1[a,b,g . (a,b)]
from BINOP_1:sch 3(A1);
A7:
for x, y being Element of Class (EqRel S) ex z being Element of Class (EqRel S) st S2[x,y,z]
proof
let x,
y be
Element of
Class (EqRel S);
ex z being Element of Class (EqRel S) st S2[x,y,z]
consider P being
object such that A8:
P in Frac S
and A9:
x = Class (
(EqRel S),
P)
by EQREL_1:def 3;
consider Q being
object such that A10:
Q in Frac S
and A11:
y = Class (
(EqRel S),
Q)
by EQREL_1:def 3;
reconsider P =
P,
Q =
Q as
Element of
Frac S by A8, A10;
Class (
(EqRel S),
(P * Q)) is
Element of
Class (EqRel S)
by EQREL_1:def 3;
hence
ex
z being
Element of
Class (EqRel S) st
S2[
x,
y,
z]
by A9, A11;
verum
end;
consider h being BinOp of (Class (EqRel S)) such that
A12:
for a, b being Element of Class (EqRel S) holds S2[a,b,h . (a,b)]
from BINOP_1:sch 3(A7);
take
doubleLoopStr(# (Class (EqRel S)),g,h,u,z #)
; ( the carrier of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) = Class (EqRel S) & 1. doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) = Class ((EqRel S),(1. (R,S))) & 0. doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) . (x,y) = Class ((EqRel S),(a * b)) ) ) )
thus
( the carrier of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) = Class (EqRel S) & 1. doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) = Class ((EqRel S),(1. (R,S))) & 0. doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of doubleLoopStr(# (Class (EqRel S)),g,h,u,z #) . (x,y) = Class ((EqRel S),(a * b)) ) ) )
by A6, A12; verum