let g be sequence of L; :: thesis:
assume A1: g = f +* ((x,y) --> (a,b)) ; :: thesis:
H0: dom ((x,y) --> (a,b)) = {x,y} by FUNCT_4:62;
then H1: dom g = (dom f) \/ {x,y} by A1, FUNCT_4:def 1;
A2: Support f is finite by POLYNOM1:def 5;

let o be object ; :: thesis:
assume o in Support g ; :: thesis:
then B0: ( o in dom g & g . o <> 0. L ) by POLYNOM1:def 3;

suppose B1: not o in {x,y} ; :: thesis:

then B2: g . o = f . o by A1, H0, FUNCT_4:11;
o in dom f by B0, B1, H1, XBOOLE_0:def 3;
then o in Support f by B2, B0, POLYNOM1:def 3;
hence o in (Support f) \/ {x,y} by XBOOLE_0:def 3; :: thesis:

end;

suppose o in {x,y} ; :: thesis:

hence o in (Support f) \/ {x,y} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then Support g c= (Support f) \/ {x,y} ;
hence g is finite-Support by A2, POLYNOM1:def 5; :: thesis: