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