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)); :: thesis: 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; :: thesis: 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 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)); :: thesis: 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 ;
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 ; :: thesis: 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 take doubleLoopStr(# (Class (EqRel (R,I))),g,h,u,z #) ; :: thesis: ( 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 ; :: thesis: verum