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 object holds
( [p,q] in R1 iff [p,q] in R2 )

proof

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

A10: now :: thesis: ( [p,q] in R2 implies [p,q] in R1 )

assume A11: [p,q] in R2 ; :: thesis: [p,q] in R1
then consider p9, q9 being object 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:2;
reconsider p9 = p9, q9 = q9 as Polynomial of n,L by A13, A14, POLYNOM1:def 11;
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 1;
A15: p = p9 by A12, XTUPLE_0:1;
A16: q = q9 by A12, XTUPLE_0:1;
p9 reduces_to q9,P,T by A8, A11, A12;
hence [p,q] in R1 by A7, A15, A16; :: thesis: verum

end;

now :: thesis: ( [p,q] in R1 implies [p,q] in R2 )

assume A17: [p,q] in R1 ; :: thesis: [p,q] in R2
then consider p9, q9 being object 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:2;
reconsider p9 = p9, q9 = q9 as Polynomial of n,L by A19, A20, POLYNOM1:def 11;
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 1;
A21: p = p9 by A18, XTUPLE_0:1;
A22: q = q9 by A18, XTUPLE_0:1;
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