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)); ( ( 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 )
; R1 = R2
for p, q being object holds
( [p,q] in R1 iff [p,q] in R2 )
proof
let p,
q be
object ;
( [p,q] in R1 iff [p,q] in R2 )
A9:
0_ (
n,
L)
= 0. (Polynom-Ring (n,L))
by POLYNOM1:def 11;
A10:
now ( [p,q] in R2 implies [p,q] in R1 )assume A11:
[p,q] in R2
;
[p,q] in R1then 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;
verum end;
now ( [p,q] in R1 implies [p,q] in R2 )assume A17:
[p,q] in R1
;
[p,q] in R2then 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;
verum end;
hence
(
[p,q] in R1 iff
[p,q] in R2 )
by A10;
verum
end;
hence
R1 = R2
by RELAT_1:def 2; verum