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

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

suppose ( x in dom f & a = x ) ; :: thesis:

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

end;

suppose ( x in dom f & a <> x ) ; :: thesis:

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:

end;

suppose not x in dom f ; :: thesis:

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:

end;

end;

end;

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