set E = EqRel (R,I);

let X, Y be strict doubleLoopStr ; :: thesis: ( the carrier of X = Class (EqRel (R,I)) & 1. X = Class ((EqRel (R,I)),(1. R)) & 0. X = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of X ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of X ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) & the carrier of Y = Class (EqRel (R,I)) & 1. Y = Class ((EqRel (R,I)),(1. R)) & 0. Y = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of Y ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of Y . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of Y ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of Y . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) implies X = Y )

assume that

A13: the carrier of X = Class (EqRel (R,I)) and

A14: ( 1. X = Class ((EqRel (R,I)),(1. R)) & 0. X = Class ((EqRel (R,I)),(0. R)) ) and

A15: for x, y being Element of X ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) ) and

A16: for x, y being Element of X ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) ) and

A17: the carrier of Y = Class (EqRel (R,I)) and

A18: ( 1. Y = Class ((EqRel (R,I)),(1. R)) & 0. Y = Class ((EqRel (R,I)),(0. R)) ) and

A19: for x, y being Element of Y ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of Y . (x,y) = Class ((EqRel (R,I)),(a + b)) ) and

A20: for x, y being Element of Y ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of Y . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ; :: thesis: X = Y

A21: for x, y being Element of X holds the multF of X . (x,y) = the multF of Y . (x,y)

hence X = Y by A13, A14, A17, A18, A21, BINOP_1:2; :: thesis: verum

let X, Y be strict doubleLoopStr ; :: thesis: ( the carrier of X = Class (EqRel (R,I)) & 1. X = Class ((EqRel (R,I)),(1. R)) & 0. X = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of X ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of X ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) & the carrier of Y = Class (EqRel (R,I)) & 1. Y = Class ((EqRel (R,I)),(1. R)) & 0. Y = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of Y ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of Y . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of Y ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of Y . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) implies X = Y )

assume that

A13: the carrier of X = Class (EqRel (R,I)) and

A14: ( 1. X = Class ((EqRel (R,I)),(1. R)) & 0. X = Class ((EqRel (R,I)),(0. R)) ) and

A15: for x, y being Element of X ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) ) and

A16: for x, y being Element of X ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) ) and

A17: the carrier of Y = Class (EqRel (R,I)) and

A18: ( 1. Y = Class ((EqRel (R,I)),(1. R)) & 0. Y = Class ((EqRel (R,I)),(0. R)) ) and

A19: for x, y being Element of Y ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of Y . (x,y) = Class ((EqRel (R,I)),(a + b)) ) and

A20: for x, y being Element of Y ex a, b being Element of R st

( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of Y . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ; :: thesis: X = Y

A21: for x, y being Element of X holds the multF of X . (x,y) = the multF of Y . (x,y)

proof

for x, y being Element of X holds the addF of X . (x,y) = the addF of Y . (x,y)
let x, y be Element of X; :: thesis: the multF of X . (x,y) = the multF of Y . (x,y)

consider a, b being Element of R such that

A22: x = Class ((EqRel (R,I)),a) and

A23: y = Class ((EqRel (R,I)),b) and

A24: the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) by A16;

consider a1, b1 being Element of R such that

A25: x = Class ((EqRel (R,I)),a1) and

A26: y = Class ((EqRel (R,I)),b1) and

A27: the multF of Y . (x,y) = Class ((EqRel (R,I)),(a1 * b1)) by A13, A17, A20;

b - b1 in I by A23, A26, Th6;

then A28: a1 * (b - b1) in I by IDEAL_1:def 2;

A29: ((a - a1) * b) + (a1 * (b - b1)) = ((a * b) - (a1 * b)) + (a1 * (b - b1)) by VECTSP_1:13

.= ((a * b) - (a1 * b)) + ((a1 * b) - (a1 * b1)) by VECTSP_1:11

.= (((a * b) - (a1 * b)) + (a1 * b)) - (a1 * b1) by RLVECT_1:28

.= (a * b) - (a1 * b1) by Th1 ;

a - a1 in I by A22, A25, Th6;

then (a - a1) * b in I by IDEAL_1:def 3;

then ((a - a1) * b) + (a1 * (b - b1)) in I by A28, IDEAL_1:def 1;

hence the multF of X . (x,y) = the multF of Y . (x,y) by A24, A27, A29, Th6; :: thesis: verum

end;consider a, b being Element of R such that

A22: x = Class ((EqRel (R,I)),a) and

A23: y = Class ((EqRel (R,I)),b) and

A24: the multF of X . (x,y) = Class ((EqRel (R,I)),(a * b)) by A16;

consider a1, b1 being Element of R such that

A25: x = Class ((EqRel (R,I)),a1) and

A26: y = Class ((EqRel (R,I)),b1) and

A27: the multF of Y . (x,y) = Class ((EqRel (R,I)),(a1 * b1)) by A13, A17, A20;

b - b1 in I by A23, A26, Th6;

then A28: a1 * (b - b1) in I by IDEAL_1:def 2;

A29: ((a - a1) * b) + (a1 * (b - b1)) = ((a * b) - (a1 * b)) + (a1 * (b - b1)) by VECTSP_1:13

.= ((a * b) - (a1 * b)) + ((a1 * b) - (a1 * b1)) by VECTSP_1:11

.= (((a * b) - (a1 * b)) + (a1 * b)) - (a1 * b1) by RLVECT_1:28

.= (a * b) - (a1 * b1) by Th1 ;

a - a1 in I by A22, A25, Th6;

then (a - a1) * b in I by IDEAL_1:def 3;

then ((a - a1) * b) + (a1 * (b - b1)) in I by A28, IDEAL_1:def 1;

hence the multF of X . (x,y) = the multF of Y . (x,y) by A24, A27, A29, Th6; :: thesis: verum

proof

then
the addF of X = the addF of Y
by A13, A17, BINOP_1:2;
let x, y be Element of X; :: thesis: the addF of X . (x,y) = the addF of Y . (x,y)

consider a, b being Element of R such that

A30: ( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) ) and

A31: the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) by A15;

consider a1, b1 being Element of R such that

A32: ( x = Class ((EqRel (R,I)),a1) & y = Class ((EqRel (R,I)),b1) ) and

A33: the addF of Y . (x,y) = Class ((EqRel (R,I)),(a1 + b1)) by A13, A17, A19;

( a - a1 in I & b - b1 in I ) by A30, A32, Th6;

then A34: (a - a1) + (b - b1) in I by IDEAL_1:def 1;

(a + b) - (a1 + b1) = ((a + b) - a1) - b1 by RLVECT_1:27

.= ((a - a1) + b) - b1 by RLVECT_1:28

.= (a - a1) + (b - b1) by RLVECT_1:28 ;

hence the addF of X . (x,y) = the addF of Y . (x,y) by A31, A33, A34, Th6; :: thesis: verum

end;consider a, b being Element of R such that

A30: ( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) ) and

A31: the addF of X . (x,y) = Class ((EqRel (R,I)),(a + b)) by A15;

consider a1, b1 being Element of R such that

A32: ( x = Class ((EqRel (R,I)),a1) & y = Class ((EqRel (R,I)),b1) ) and

A33: the addF of Y . (x,y) = Class ((EqRel (R,I)),(a1 + b1)) by A13, A17, A19;

( a - a1 in I & b - b1 in I ) by A30, A32, Th6;

then A34: (a - a1) + (b - b1) in I by IDEAL_1:def 1;

(a + b) - (a1 + b1) = ((a + b) - a1) - b1 by RLVECT_1:27

.= ((a - a1) + b) - b1 by RLVECT_1:28

.= (a - a1) + (b - b1) by RLVECT_1:28 ;

hence the addF of X . (x,y) = the addF of Y . (x,y) by A31, A33, A34, Th6; :: thesis: verum

hence X = Y by A13, A14, A17, A18, A21, BINOP_1:2; :: thesis: verum