defpred S1[ object , object ] means ex p1, p2 being Polynomial of n,L st
( p1 = n `1 & n `2 = p2 & p1 in P & p2 in P & T = S-Poly (p1,p2,T) );
A1:
for x being object st x in [:P,P:] holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in [:P,P:] implies ex y being object st S1[x,y] )
assume
x in [:P,P:]
;
ex y being object st S1[x,y]
then consider p1,
p2 being
object such that A2:
(
p1 in P &
p2 in P )
and A3:
[p1,p2] = x
by ZFMISC_1:def 2;
reconsider p1 =
p1,
p2 =
p2 as
Polynomial of
n,
L by A2, POLYNOM1:def 11;
take
S-Poly (
p1,
p2,
T)
;
S1[x, S-Poly (p1,p2,T)]
take
p1
;
ex p2 being Polynomial of n,L st
( p1 = x `1 & x `2 = p2 & p1 in P & p2 in P & S-Poly (p1,p2,T) = S-Poly (p1,p2,T) )
take
p2
;
( p1 = x `1 & x `2 = p2 & p1 in P & p2 in P & S-Poly (p1,p2,T) = S-Poly (p1,p2,T) )
thus
x `1 = p1
by A3;
( x `2 = p2 & p1 in P & p2 in P & S-Poly (p1,p2,T) = S-Poly (p1,p2,T) )
thus
x `2 = p2
by A3;
( p1 in P & p2 in P & S-Poly (p1,p2,T) = S-Poly (p1,p2,T) )
thus
(
p1 in P &
p2 in P &
S-Poly (
p1,
p2,
T)
= S-Poly (
p1,
p2,
T) )
by A2;
verum
end;
consider f being Function such that
A4:
( dom f = [:P,P:] & ( for x being object st x in [:P,P:] holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A1);
A5:
now for v being object st v in S-Poly (P,T) holds
v in rng flet v be
object ;
( v in S-Poly (P,T) implies v in rng f )assume
v in S-Poly (
P,
T)
;
v in rng fthen consider p1,
p2 being
Polynomial of
n,
L such that A6:
v = S-Poly (
p1,
p2,
T)
and A7:
(
p1 in P &
p2 in P )
;
A8:
[p1,p2] in dom f
by A4, A7, ZFMISC_1:def 2;
then consider p19,
p29 being
Polynomial of
n,
L such that A9:
(
[p1,p2] `1 = p19 &
[p1,p2] `2 = p29 )
and
p19 in P
and
p29 in P
and A10:
f . [p1,p2] = S-Poly (
p19,
p29,
T)
by A4;
(
p1 = p19 &
p2 = p29 )
by A9;
hence
v in rng f
by A6, A8, A10, FUNCT_1:def 3;
verum end;
then
rng f = S-Poly (P,T)
by A5, TARSKI:2;
hence
S-Poly (P,T) is finite
by A4, FINSET_1:8; verum