let P1, P2 be non empty strict doubleLoopStr ; ( ( 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 )
; P1 = P2
then A21:
the carrier of P1 = the carrier of P2
by TARSKI:2;
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; verum