defpred S1[ object , object ] means ex p, q being Polynomial of n,L st
( p = $1 & q = $2 & p reduces_to q,P,T );
set A = NonZero (Polynom-Ring (n,L));
set B = the carrier of (Polynom-Ring (n,L));
consider R being Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) such that
A1:
for x, y being object holds
( [x,y] in R iff ( x in NonZero (Polynom-Ring (n,L)) & y in the carrier of (Polynom-Ring (n,L)) & S1[x,y] ) )
from RELSET_1:sch 1();
take
R
; for p, q being Polynomial of n,L holds
( [p,q] in R iff p reduces_to q,P,T )
now for p, q being Polynomial of n,L holds
( [p,q] in R iff p reduces_to q,P,T )let p,
q be
Polynomial of
n,
L;
( [p,q] in R iff p reduces_to q,P,T )A2:
now ( p reduces_to q,P,T implies [p,q] in R )assume A3:
p reduces_to q,
P,
T
;
[p,q] in Rthen consider pp being
Polynomial of
n,
L such that
pp in P
and A4:
p reduces_to q,
pp,
T
;
ex
b being
bag of
n st
p reduces_to q,
pp,
b,
T
by A4;
then
p <> 0_ (
n,
L)
;
then A5:
not
p in {(0_ (n,L))}
by TARSKI:def 1;
A6:
q in the
carrier of
(Polynom-Ring (n,L))
by POLYNOM1:def 11;
(
0_ (
n,
L)
= 0. (Polynom-Ring (n,L)) &
p in the
carrier of
(Polynom-Ring (n,L)) )
by POLYNOM1:def 11;
then
p in NonZero (Polynom-Ring (n,L))
by A5, XBOOLE_0:def 5;
hence
[p,q] in R
by A1, A3, A6;
verum end; hence
(
[p,q] in R iff
p reduces_to q,
P,
T )
by A2;
verum end;
hence
for p, q being Polynomial of n,L holds
( [p,q] in R iff p reduces_to q,P,T )
; verum