let f be Function; :: thesis: for x, y being object holds support (f +* (x .--> y)) c= (support f) \/ {x}
let x, y be object ; :: thesis: support (f +* (x .--> y)) c= (support f) \/ {x}
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 PRE_POLY: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:83;
then a in support f by A1, PRE_POLY:def 7;
hence a in (support f) \/ {x} by XBOOLE_0:def 3; :: thesis: verum
end;
end;