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

A20: now :: thesis: for x being object holds
( 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;

then A21: the carrier of P1 = the carrier of P2 by TARSKI:2;

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)

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;

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)

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;

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