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 ; :: thesis: ( x in [:P,P:] implies ex y being object st S1[x,y] )
assume x in [:P,P:] ; :: thesis: 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 ;
take S-Poly (p1,p2,T) ; :: thesis: S1[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;
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
A5: now :: thesis: for v being object st v in S-Poly (P,T) holds
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 ;
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 ; :: thesis: verum
end;
now :: thesis: for v being object st v in rng f holds
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 ;
hence v in S-Poly (P,T) by A12; :: thesis: verum
end;
then rng f = S-Poly (P,T) by ;
hence S-Poly (P,T) is finite by ; :: thesis: verum