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