set F = f +* (x,y);
support (f +* (x,y)) c= (support f) \/ {x}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in support (f +* (x,y)) or a in (support f) \/ {x} )
assume a in support (f +* (x,y)) ; :: thesis: a in (support f) \/ {x}
then A1: (f +* (x,y)) . a <> 0 by Def7;

per cases ( ( x in dom f & a = x ) or ( x in dom f & a <> x ) or not x in dom f ) ;

suppose ( x in dom f & a = x ) ; :: thesis: a in (support f) \/ {x}

then a in {x} by TARSKI:def 1;
hence a in (support f) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( x in dom f & a <> x ) ; :: thesis: a in (support f) \/ {x}

then (f +* (x,y)) . a = f . a by FUNCT_7:32;
then a in support f by A1, Def7;
hence a in (support f) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: a in (support f) \/ {x}

then (f +* (x,y)) . a = f . a by FUNCT_7:def 3;
then a in support f by A1, Def7;
hence a in (support f) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence support (f +* (x,y)) is finite ; :: according to PRE_POLY:def 8 :: thesis: verum