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
A22: for x being set holds
( x in the carrier of it1 iff x is Polynomial of n,L ) 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: 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
A25: 0. it1 = 0_ n,L and
A26: 1. it1 = 1_ n,L and
A27: for x being set holds
( x in the carrier of it2 iff x is Polynomial of n,L ) and
A28: 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
A29: 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
A30: 0. it2 = 0_ n,L and
A31: 1. it2 = 1_ n,L ; :: thesis: it1 = it2

A32: now

let x be set ; :: 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 A22;
hence x in the carrier of it2 by A27; :: 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 A27;
hence x in the carrier of it1 by A22; :: thesis: verum

end;

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

now

let a, b be Element of it1; :: thesis: the addF of it1 . a,b = the addF of it2 . a,b
reconsider a1 = a, b1 = b as Element of it1 ;
reconsider p = a, q = b as Polynomial of n,L by A22;
reconsider a' = a, b' = b as Element of it2 by A32;
reconsider a1' = a', b1' = b' as Element of it2 ;
thus the addF of it1 . a,b = a1 + b1
.= p + q by A23
.= a1' + b1' by A28
.= the addF of it2 . a,b ; :: thesis: verum

end;

then A34: the addF of it1 = the addF of it2 by A33, BINOP_1:2;

now

let a, b be Element of it1; :: thesis: the multF of it1 . a,b = the multF of it2 . a,b
reconsider a1 = a, b1 = b as Element of it1 ;
reconsider p = a, q = b as Polynomial of n,L by A22;
reconsider a' = a, b' = b as Element of it2 by A32;
reconsider a1' = a', b1' = b' as Element of it2 ;
thus the multF of it1 . a,b = a1 * b1
.= p *' q by A24
.= a1' * b1' by A29
.= the multF of it2 . a,b ; :: thesis: verum

end;

hence it1 = it2 by A25, A26, A30, A31, A33, A34, BINOP_1:2; :: thesis: verum