defpred S_{1}[ 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 S_{1}[x,y]

A4: ( dom f = [:P,P:] & ( for x being object st x in [:P,P:] holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A1);

hence S-Poly (P,T) is finite by A4, FINSET_1:8; :: thesis: verum

( 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 S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in [:P,P:] implies ex y being object st S_{1}[x,y] )

assume x in [:P,P:] ; :: thesis: ex y being object st S_{1}[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) ; :: thesis: S_{1}[x, S-Poly (p1,p2,T)]

take p1 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: verum

end;assume x in [:P,P:] ; :: thesis: ex y being object st S

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) ; :: thesis: S

take p1 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: verum

A4: ( dom f = [:P,P:] & ( for x being object st x in [:P,P:] holds

S

A5: now :: thesis: for v being object st v in S-Poly (P,T) holds

v in rng f

v in rng f

let v be object ; :: thesis: ( v in S-Poly (P,T) implies v in rng f )

assume v in S-Poly (P,T) ; :: thesis: v in rng f

then 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; :: thesis: verum

end;assume v in S-Poly (P,T) ; :: thesis: v in rng f

then 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; :: thesis: verum

now :: thesis: for v being object st v in rng f holds

v in S-Poly (P,T)

then
rng f = S-Poly (P,T)
by A5, TARSKI:2;v in S-Poly (P,T)

let v be object ; :: thesis: ( v in rng f implies v in S-Poly (P,T) )

assume v in rng f ; :: thesis: v in S-Poly (P,T)

then consider u being object such that

A11: u in dom f and

A12: v = f . u by FUNCT_1:def 3;

ex p1, p2 being Polynomial of n,L st

( p1 = u `1 & u `2 = p2 & p1 in P & p2 in P & f . u = S-Poly (p1,p2,T) ) by A4, A11;

hence v in S-Poly (P,T) by A12; :: thesis: verum

end;assume v in rng f ; :: thesis: v in S-Poly (P,T)

then consider u being object such that

A11: u in dom f and

A12: v = f . u by FUNCT_1:def 3;

ex p1, p2 being Polynomial of n,L st

( p1 = u `1 & u `2 = p2 & p1 in P & p2 in P & f . u = S-Poly (p1,p2,T) ) by A4, A11;

hence v in S-Poly (P,T) by A12; :: thesis: verum

hence S-Poly (P,T) is finite by A4, FINSET_1:8; :: thesis: verum