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 5;
reconsider z = Class (EqRel R,I),(0. R) as Element of Class (EqRel R,I) by EQREL_1:def 5;
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
set such that A2:
P in the
carrier of
R
and A3:
x = Class (EqRel R,I),
P
by EQREL_1:def 5;
consider Q being
set such that A4:
Q in the
carrier of
R
and A5:
y = Class (EqRel R,I),
Q
by EQREL_1:def 5;
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 5;
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
set such that A8:
P in the
carrier of
R
and A9:
x = Class (EqRel R,I),
P
by EQREL_1:def 5;
consider Q being
set such that A10:
Q in the
carrier of
R
and A11:
y = Class (EqRel R,I),
Q
by EQREL_1:def 5;
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 5;
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 G = doubleLoopStr(# (Class (EqRel R,I)),g,h,u,z #); ( the carrier of G = Class (EqRel R,I) & 1. G = Class (EqRel R,I),(1. R) & 0. G = Class (EqRel R,I),(0. R) & ( for x, y being Element of G ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of G . x,y = Class (EqRel R,I),(a + b) ) ) & ( for x, y being Element of G ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of G . x,y = Class (EqRel R,I),(a * b) ) ) )
thus
( the carrier of G = Class (EqRel R,I) & 1. G = Class (EqRel R,I),(1. R) & 0. G = Class (EqRel R,I),(0. R) & ( for x, y being Element of G ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of G . x,y = Class (EqRel R,I),(a + b) ) ) & ( for x, y being Element of G ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of G . x,y = Class (EqRel R,I),(a * b) ) ) )
by A6, A12; verum