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
set A = NonZero (Polynom-Ring n,L);
set B = the carrier of (Polynom-Ring n,L);
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 )
X:
0_ n,
L = 0. (Polynom-Ring n,L)
by POLYNOM1:def 27;
A9:
now assume A10:
[p,q] in R1
;
:: thesis: [p,q] in R2then consider p',
q' being
set such that A11:
(
[p,q] = [p',q'] &
p' in NonZero (Polynom-Ring n,L) &
q' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
reconsider p' =
p',
q' =
q' as
Polynomial of
n,
L by A11, POLYNOM1:def 27;
not
p' in {(0_ n,L)}
by A11, X, XBOOLE_0:def 5;
then
p' <> 0_ n,
L
by TARSKI:def 1;
then reconsider p' =
p' as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
A12:
p' reduces_to q',
P,
T
by A7, A10, A11;
A13:
p =
[p',q'] `1
by A11, MCART_1:def 1
.=
p'
by MCART_1:def 1
;
q =
[p',q'] `2
by A11, MCART_1:def 2
.=
q'
by MCART_1:def 2
;
hence
[p,q] in R2
by A8, A12, A13;
:: thesis: verum end;
now assume A14:
[p,q] in R2
;
:: thesis: [p,q] in R1then consider p',
q' being
set such that A15:
(
[p,q] = [p',q'] &
p' in NonZero (Polynom-Ring n,L) &
q' in the
carrier of
(Polynom-Ring n,L) )
by RELSET_1:6;
reconsider p' =
p',
q' =
q' as
Polynomial of
n,
L by A15, POLYNOM1:def 27;
not
p' in {(0_ n,L)}
by A15, X, XBOOLE_0:def 5;
then
p' <> 0_ n,
L
by TARSKI:def 1;
then reconsider p' =
p' as
non-zero Polynomial of
n,
L by POLYNOM7:def 2;
A16:
p' reduces_to q',
P,
T
by A8, A14, A15;
A17:
p =
[p',q'] `1
by A15, MCART_1:def 1
.=
p'
by MCART_1:def 1
;
q =
[p',q'] `2
by A15, MCART_1:def 2
.=
q'
by MCART_1:def 2
;
hence
[p,q] in R1
by A7, A16, A17;
:: thesis: verum end;
hence
(
[p,q] in R1 iff
[p,q] in R2 )
by A9;
:: thesis: verum
end;
hence
R1 = R2
by RELAT_1:def 2; :: thesis: verum