let P1, P2 be non empty strict doubleLoopStr ; :: thesis: ( ( for x being set holds

( x in the carrier of P1 iff x is Polynomial of L ) ) & ( for x, y being Element of P1

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of P1

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. P1 = 0_. L & 1. P1 = 1_. L & ( for x being set holds

( x in the carrier of P2 iff x is Polynomial of L ) ) & ( for x, y being Element of P2

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of P2

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. P2 = 0_. L & 1. P2 = 1_. L implies P1 = P2 )

assume that

A12: for x being set holds

( x in the carrier of P1 iff x is Polynomial of L ) and

A13: for x, y being Element of P1

for p, q being sequence of L st x = p & y = q holds

x + y = p + q and

A14: for x, y being Element of P1

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q and

A15: ( 0. P1 = 0_. L & 1. P1 = 1_. L ) and

A16: for x being set holds

( x in the carrier of P2 iff x is Polynomial of L ) and

A17: for x, y being Element of P2

for p, q being sequence of L st x = p & y = q holds

x + y = p + q and

A18: for x, y being Element of P2

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q and

A19: ( 0. P2 = 0_. L & 1. P2 = 1_. L ) ; :: thesis: P1 = P2

hence P1 = P2 by A15, A19, A21, A22, BINOP_1:2; :: thesis: verum

( x in the carrier of P1 iff x is Polynomial of L ) ) & ( for x, y being Element of P1

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of P1

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. P1 = 0_. L & 1. P1 = 1_. L & ( for x being set holds

( x in the carrier of P2 iff x is Polynomial of L ) ) & ( for x, y being Element of P2

for p, q being sequence of L st x = p & y = q holds

x + y = p + q ) & ( for x, y being Element of P2

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q ) & 0. P2 = 0_. L & 1. P2 = 1_. L implies P1 = P2 )

assume that

A12: for x being set holds

( x in the carrier of P1 iff x is Polynomial of L ) and

A13: for x, y being Element of P1

for p, q being sequence of L st x = p & y = q holds

x + y = p + q and

A14: for x, y being Element of P1

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q and

A15: ( 0. P1 = 0_. L & 1. P1 = 1_. L ) and

A16: for x being set holds

( x in the carrier of P2 iff x is Polynomial of L ) and

A17: for x, y being Element of P2

for p, q being sequence of L st x = p & y = q holds

x + y = p + q and

A18: for x, y being Element of P2

for p, q being sequence of L st x = p & y = q holds

x * y = p *' q and

A19: ( 0. P2 = 0_. L & 1. P2 = 1_. L ) ; :: thesis: P1 = P2

A20: now :: thesis: for x being object holds

( x in the carrier of P1 iff x in the carrier of P2 )

then A21:
the carrier of P1 = the carrier of P2
by TARSKI:2;( x in the carrier of P1 iff x in the carrier of P2 )

let x be object ; :: thesis: ( x in the carrier of P1 iff x in the carrier of P2 )

( x in the carrier of P1 iff x is Polynomial of L ) by A12;

hence ( x in the carrier of P1 iff x in the carrier of P2 ) by A16; :: thesis: verum

end;( x in the carrier of P1 iff x is Polynomial of L ) by A12;

hence ( x in the carrier of P1 iff x in the carrier of P2 ) by A16; :: thesis: verum

A22: now :: thesis: for x being Element of P1

for y being Element of P2 holds the multF of P1 . (x,y) = the multF of P2 . (x,y)

for y being Element of P2 holds the multF of P1 . (x,y) = the multF of P2 . (x,y)

let x be Element of P1; :: thesis: for y being Element of P2 holds the multF of P1 . (x,y) = the multF of P2 . (x,y)

let y be Element of P2; :: thesis: the multF of P1 . (x,y) = the multF of P2 . (x,y)

reconsider y1 = y as Element of P1 by A20;

reconsider x1 = x as Element of P2 by A20;

reconsider p = x as sequence of L by A12;

reconsider q = y as sequence of L by A16;

thus the multF of P1 . (x,y) = x * y1

.= p *' q by A14

.= x1 * y by A18

.= the multF of P2 . (x,y) ; :: thesis: verum

end;let y be Element of P2; :: thesis: the multF of P1 . (x,y) = the multF of P2 . (x,y)

reconsider y1 = y as Element of P1 by A20;

reconsider x1 = x as Element of P2 by A20;

reconsider p = x as sequence of L by A12;

reconsider q = y as sequence of L by A16;

thus the multF of P1 . (x,y) = x * y1

.= p *' q by A14

.= x1 * y by A18

.= the multF of P2 . (x,y) ; :: thesis: verum

now :: thesis: for x being Element of P1

for y being Element of P2 holds the addF of P1 . (x,y) = the addF of P2 . (x,y)

then
the addF of P1 = the addF of P2
by A21, BINOP_1:2;for y being Element of P2 holds the addF of P1 . (x,y) = the addF of P2 . (x,y)

let x be Element of P1; :: thesis: for y being Element of P2 holds the addF of P1 . (x,y) = the addF of P2 . (x,y)

let y be Element of P2; :: thesis: the addF of P1 . (x,y) = the addF of P2 . (x,y)

reconsider y1 = y as Element of P1 by A20;

reconsider x1 = x as Element of P2 by A20;

reconsider p = x as sequence of L by A12;

reconsider q = y as sequence of L by A16;

thus the addF of P1 . (x,y) = x + y1

.= p + q by A13

.= x1 + y by A17

.= the addF of P2 . (x,y) ; :: thesis: verum

end;let y be Element of P2; :: thesis: the addF of P1 . (x,y) = the addF of P2 . (x,y)

reconsider y1 = y as Element of P1 by A20;

reconsider x1 = x as Element of P2 by A20;

reconsider p = x as sequence of L by A12;

reconsider q = y as sequence of L by A16;

thus the addF of P1 . (x,y) = x + y1

.= p + q by A13

.= x1 + y by A17

.= the addF of P2 . (x,y) ; :: thesis: verum

hence P1 = P2 by A15, A19, A21, A22, BINOP_1:2; :: thesis: verum