let it1, it2 be non empty strict doubleLoopStr ; :: thesis: ( ( for x being set holds
( x in the carrier of it1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of it1
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it1
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. it1 = 0_ (n,L) & 1. it1 = 1_ (n,L) & ( for x being set holds
( x in the carrier of it2 iff x is Polynomial of n,L ) ) & ( for x, y being Element of it2
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it2
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. it2 = 0_ (n,L) & 1. it2 = 1_ (n,L) implies it1 = it2 )
assume that
A21: for x being set holds
( x in the carrier of it1 iff x is Polynomial of n,L ) and
A22: for x, y being Element of it1
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q and
A23: for x, y being Element of it1
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q and
A24: ( 0. it1 = 0_ (n,L) & 1. it1 = 1_ (n,L) ) and
A25: for x being set holds
( x in the carrier of it2 iff x is Polynomial of n,L ) and
A26: for x, y being Element of it2
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q and
A27: for x, y being Element of it2
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q and
A28: ( 0. it2 = 0_ (n,L) & 1. it2 = 1_ (n,L) ) ; :: thesis: it1 = it2

A29: now :: thesis: for x being object holds
( ( x in the carrier of it1 implies x in the carrier of it2 ) & ( x in the carrier of it2 implies x in the carrier of it1 ) )

let x be object ; :: thesis: ( ( x in the carrier of it1 implies x in the carrier of it2 ) & ( x in the carrier of it2 implies x in the carrier of it1 ) )

hereby :: thesis: ( x in the carrier of it2 implies x in the carrier of it1 )

assume x in the carrier of it1 ; :: thesis: x in the carrier of it2
then x is Polynomial of n,L by A21;
hence x in the carrier of it2 by A25; :: thesis: verum

end;

assume x in the carrier of it2 ; :: thesis: x in the carrier of it1
then x is Polynomial of n,L by A25;
hence x in the carrier of it1 by A21; :: thesis: verum

end;

then A30: the carrier of it1 = the carrier of it2 by TARSKI:2;

A31: now :: thesis: for a, b being Element of it1 holds the multF of it1 . (a,b) = the multF of it2 . (a,b)

let a, b be Element of it1; :: thesis: the multF of it1 . (a,b) = the multF of it2 . (a,b)
reconsider a9 = a, b9 = b as Element of it2 by A29;
reconsider a19 = a9, b19 = b9 as Element of it2 ;
reconsider p = a, q = b as Polynomial of n,L by A21;
reconsider a1 = a, b1 = b as Element of it1 ;
thus the multF of it1 . (a,b) = a1 * b1
.= p *' q by A23
.= a19 * b19 by A27
.= the multF of it2 . (a,b) ; :: thesis: verum

end;

now :: thesis: for a, b being Element of it1 holds the addF of it1 . (a,b) = the addF of it2 . (a,b)

let a, b be Element of it1; :: thesis: the addF of it1 . (a,b) = the addF of it2 . (a,b)
reconsider a9 = a, b9 = b as Element of it2 by A29;
reconsider a19 = a9, b19 = b9 as Element of it2 ;
reconsider p = a, q = b as Polynomial of n,L by A21;
reconsider a1 = a, b1 = b as Element of it1 ;
thus the addF of it1 . (a,b) = a1 + b1
.= p + q by A22
.= a19 + b19 by A26
.= the addF of it2 . (a,b) ; :: thesis: verum

end;

then the addF of it1 = the addF of it2 by A30, BINOP_1:2;
hence it1 = it2 by A24, A28, A30, A31, BINOP_1:2; :: thesis: verum