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;

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;