let g be sequence of L; :: thesis: ( g = f +* ((x,y) --> (a,b)) implies g is finite-Support )
assume A1: g = f +* ((x,y) --> (a,b)) ; :: thesis: g is finite-Support
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;

now :: thesis: for o being object st o in Support g holds
o in (Support f) \/ {x,y}

let o be object ; :: thesis: ( o in Support g implies b₁ in (Support f) \/ {x,y} )
assume o in Support g ; :: thesis: b₁ in (Support f) \/ {x,y}
then B0: ( o in dom g & g . o <> 0. L ) by POLYNOM1:def 3;

per cases ( not o in {x,y} or o in {x,y} ) ;

suppose B1: not o in {x,y} ; :: thesis: b₁ in (Support f) \/ {x,y}

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: verum

end;

suppose o in {x,y} ; :: thesis: b₁ in (Support f) \/ {x,y}

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

end;

end;

end;

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