let g be sequence of L; ( g = f +* ((x,y) --> (a,b)) implies g is finite-Support )
assume A1:
g = f +* ((x,y) --> (a,b))
; 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;
then
Support g c= (Support f) \/ {x,y}
;
hence
g is finite-Support
by A2, POLYNOM1:def 5; verum