set A = NonZero (Polynom-Ring n,L);
set B = the carrier of (Polynom-Ring n,L);
let R1, R2 be Relation of (NonZero (Polynom-Ring n,L)),the carrier of (Polynom-Ring n,L); :: thesis: ( ( for p, q being Polynomial of n,L holds
( [p,q] in R1 iff p reduces_to q,P,T ) ) & ( for p, q being Polynomial of n,L holds
( [p,q] in R2 iff p reduces_to q,P,T ) ) implies R1 = R2 )
assume that
A7: for p, q being Polynomial of n,L holds
( [p,q] in R1 iff p reduces_to q,P,T ) and
A8: for p, q being Polynomial of n,L holds
( [p,q] in R2 iff p reduces_to q,P,T ) ; :: thesis: R1 = R2
for p, q being set holds
( [p,q] in R1 iff [p,q] in R2 )

proof

let p, q be set ; :: thesis: ( [p,q] in R1 iff [p,q] in R2 )
A9: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;

A10: now

assume A11: [p,q] in R2 ; :: thesis: [p,q] in R1
then consider p9, q9 being set such that
A12: [p,q] = [p9,q9] and
A13: p9 in NonZero (Polynom-Ring n,L) and
A14: q9 in the carrier of (Polynom-Ring n,L) by RELSET_1:6;
reconsider p9 = p9, q9 = q9 as Polynomial of n,L by A13, A14, POLYNOM1:def 27;
not p9 in {(0_ n,L)} by A9, A13, XBOOLE_0:def 5;
then p9 <> 0_ n,L by TARSKI:def 1;
then reconsider p9 = p9 as non-zero Polynomial of n,L by POLYNOM7:def 2;
A15: p = [p9,q9] `1 by A12, MCART_1:def 1
.= p9 by MCART_1:def 1 ;
A16: q = [p9,q9] `2 by A12, MCART_1:def 2
.= q9 by MCART_1:def 2 ;
p9 reduces_to q9,P,T by A8, A11, A12;
hence [p,q] in R1 by A7, A15, A16; :: thesis: verum

end;

now

assume A17: [p,q] in R1 ; :: thesis: [p,q] in R2
then consider p9, q9 being set such that
A18: [p,q] = [p9,q9] and
A19: p9 in NonZero (Polynom-Ring n,L) and
A20: q9 in the carrier of (Polynom-Ring n,L) by RELSET_1:6;
reconsider p9 = p9, q9 = q9 as Polynomial of n,L by A19, A20, POLYNOM1:def 27;
not p9 in {(0_ n,L)} by A9, A19, XBOOLE_0:def 5;
then p9 <> 0_ n,L by TARSKI:def 1;
then reconsider p9 = p9 as non-zero Polynomial of n,L by POLYNOM7:def 2;
A21: p = [p9,q9] `1 by A18, MCART_1:def 1
.= p9 by MCART_1:def 1 ;
A22: q = [p9,q9] `2 by A18, MCART_1:def 2
.= q9 by MCART_1:def 2 ;
p9 reduces_to q9,P,T by A7, A17, A18;
hence [p,q] in R2 by A8, A21, A22; :: thesis: verum

end;

hence ( [p,q] in R1 iff [p,q] in R2 ) by A10; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum