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
A18: for x being set holds
( x in the carrier of P1 iff x is Polynomial of L ) and
A19: 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
A20: 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
A21: 0. P1 = 0_. L and
A22: 1. P1 = 1_. L and
A23: for x being set holds
( x in the carrier of P2 iff x is Polynomial of L ) and
A24: 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
A25: 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
A26: 0. P2 = 0_. L and
A27: 1. P2 = 1_. L ; :: thesis: P1 = P2

A28: now

let x be set ; :: 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 A18;
hence ( x in the carrier of P1 iff x in the carrier of P2 ) by A23; :: thesis: verum

end;

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

now

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 x1 = x as Element of P2 by A28;
reconsider y1 = y as Element of P1 by A28;
reconsider p = x as sequence of L by A18;
reconsider q = y as sequence of L by A23;
thus the addF of P1 . x,y = x + y1
.= p + q by A19
.= x1 + y by A24
.= the addF of P2 . x,y ; :: thesis: verum

end;

then A30: the addF of P1 = the addF of P2 by A29, BINOP_1:2;

now

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 x1 = x as Element of P2 by A28;
reconsider y1 = y as Element of P1 by A28;
reconsider p = x as sequence of L by A18;
reconsider q = y as sequence of L by A23;
thus the multF of P1 . x,y = x * y1
.= p *' q by A20
.= x1 * y by A25
.= the multF of P2 . x,y ; :: thesis: verum

end;

hence P1 = P2 by A21, A22, A26, A27, A29, A30, BINOP_1:2; :: thesis: verum