let f be Function; :: thesis: for x, y being object holds rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}
let x, y be object ; :: thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}

per cases ( not x in rng f or ( x in rng f & x = y ) or x <> y ) ;

suppose A1: not x in rng f ; :: thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}

then f +~ (x,y) = f by Th103;
then rng (f +~ (x,y)) = (rng f) \ {x} by A1, ZFMISC_1:57;
hence rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by XBOOLE_1:7; :: thesis: verum

end;

suppose that A2: x in rng f and
A3: x = y ; :: thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}

f +~ (x,y) = f by A3, Th102;
hence rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by A2, A3, ZFMISC_1:116; :: thesis: verum

end;

suppose A4: x <> y ; :: thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}

not x in rng (f +~ (x,y)) by A4, Th100;
then A5: (rng (f +~ (x,y))) \ {x} = rng (f +~ (x,y)) by ZFMISC_1:57;
rng (x .--> y) = {y} by FUNCOP_1:8;
then A6: (rng f) \/ (rng ((x .--> y) * f)) c= (rng f) \/ {y} by RELAT_1:26, XBOOLE_1:9;
rng (f +~ (x,y)) c= (rng f) \/ (rng ((x .--> y) * f)) by Th17;
then rng (f +~ (x,y)) c= (rng f) \/ {y} by A6;
then rng (f +~ (x,y)) c= ((rng f) \/ {y}) \ {x} by A5, XBOOLE_1:33;
hence rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by A4, ZFMISC_1:123; :: thesis: verum

end;

end;