set E = EqRel (R,I);

set A = Class (EqRel (R,I));

defpred S_{1}[ 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 S_{2}[ 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 S_{1}[x,y,z]

A6: for a, b being Element of Class (EqRel (R,I)) holds S_{1}[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 S_{2}[x,y,z]

A12: for a, b being Element of Class (EqRel (R,I)) holds S_{2}[a,b,h . (a,b)]
from BINOP_1:sch 3(A7);

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 A6, A12; :: thesis: verum

set A = Class (EqRel (R,I));

defpred S

( $1 = Class ((EqRel (R,I)),P) & $2 = Class ((EqRel (R,I)),Q) & $3 = Class ((EqRel (R,I)),(P + Q)) );

defpred S

( $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 S

proof

consider g being BinOp of (Class (EqRel (R,I))) such that
let x, y be Element of Class (EqRel (R,I)); :: thesis: ex z being Element of Class (EqRel (R,I)) st S_{1}[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 S_{1}[x,y,z]
by A3, A5; :: thesis: verum

end;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 S

A6: for a, b being Element of Class (EqRel (R,I)) holds S

A7: for x, y being Element of Class (EqRel (R,I)) ex z being Element of Class (EqRel (R,I)) st S

proof

consider h being BinOp of (Class (EqRel (R,I))) such that
let x, y be Element of Class (EqRel (R,I)); :: thesis: ex z being Element of Class (EqRel (R,I)) st S_{2}[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 S_{2}[x,y,z]
by A9, A11; :: thesis: verum

end;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 S

A12: for a, b being Element of Class (EqRel (R,I)) holds S

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 A6, A12; :: thesis: verum