defpred S₁[ 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₁[x,y]

let x be object ; :: thesis:
assume x in [:P,P:] ; :: thesis:
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:
take p1 ; :: thesis:
take p2 ; :: thesis:
thus x `1 = p1 by A3; :: thesis:
thus x `2 = p2 by A3; :: thesis:
thus ( p1 in P & p2 in P & S-Poly (p1,p2,T) = S-Poly (p1,p2,T) ) by A2; :: thesis:

end;

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

let v be object ; :: thesis:
assume v in S-Poly (P,T) ; :: thesis:
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:

end;

let v be object ; :: thesis:
assume v in rng f ; :: thesis:
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:

end;