let f be Function; :: thesis: for x, y being set holds support (f +* (x .--> y)) c= (support f) \/ {x}
let x, y be set ; :: thesis: support (f +* (x .--> y)) c= (support f) \/ {x}
let a be set ; :: 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 POLYNOM1:def 7;

per cases ( a = x or a <> x ) ;

suppose 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 a <> x ; :: thesis: a in (support f) \/ {x}

then (f +* (x .--> y)) . a = f . a by FUNCT_4:88;
then a in support f by A1, POLYNOM1:def 7;
hence a in (support f) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

end;