defpred S₁[ set , set ] 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 );
A2: for x being set st x in [:P,P:] holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in [:P,P:] implies ex y being set st S₁[x,y] )
assume x in [:P,P:] ; :: thesis: ex y being set st S₁[x,y]
then consider p1, p2 being set such that
A3: ( p1 in P & p2 in P & [p1,p2] = x ) by ZFMISC_1:def 2;
reconsider p1 = p1, p2 = p2 as Polynomial of n,L by A3, POLYNOM1:def 27;
take S-Poly p1,p2,T ; :: thesis: S₁[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, MCART_1:def 1; :: 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, MCART_1:def 2; :: 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 A3; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = [:P,P:] & ( for x being set st x in [:P,P:] holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);

A5: now

let v be set ; :: 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 set such that
A6: ( u in dom f & v = f . u ) by FUNCT_1:def 5;
consider p1, p2 being Polynomial of n,L such that
A7: ( p1 = u `1 & u `2 = p2 & p1 in P & p2 in P & f . u = S-Poly p1,p2,T ) by A4, A6;
thus v in S-Poly P,T by A6, A7; :: thesis: verum

end;

now

let v be set ; :: 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
A8: ( v = S-Poly p1,p2,T & p1 in P & p2 in P ) ;
A9: [p1,p2] in dom f by A4, A8, ZFMISC_1:def 2;
then consider p1', p2' being Polynomial of n,L such that
A10: ( [p1,p2] `1 = p1' & [p1,p2] `2 = p2' & p1' in P & p2' in P & f . [p1,p2] = S-Poly p1',p2',T ) by A4;
( p1 = p1' & p2 = p2' ) by A10, MCART_1:def 1, MCART_1:def 2;
hence v in rng f by A8, A9, A10, FUNCT_1:def 5; :: thesis: verum

end;

then rng f = S-Poly P,T by A5, TARSKI:2;
hence S-Poly P,T is finite by A4, FINSET_1:26; :: thesis: verum