let f be Function; :: thesis: for x, y being set st not x in rng f holds
f +~ (x,y) = f
let x, y be set ; :: thesis: ( not x in rng f implies f +~ (x,y) = f )
A1: dom (x .--> y) = {x} by FUNCOP_1:13;
assume not x in rng f ; :: thesis: f +~ (x,y) = f
then dom (x .--> y) misses rng f by A1, ZFMISC_1:50;
then (x .--> y) * f = {} by RELAT_1:44;
hence f +~ (x,y) = f by Th22; :: thesis: verum