let f be Function; :: thesis: for x, y being set holds rng (f +~ x,y) c= ((rng f) \ {x}) \/ {y}
let x, y be set ; :: 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 S: not x in rng f ; :: thesis: rng (f +~ x,y) c= ((rng f) \ {x}) \/ {y}

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

end;

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

f +~ x,y = f by TH1, S2;
hence rng (f +~ x,y) c= ((rng f) \ {x}) \/ {y} by S1, S2, ZFMISC_1:140; :: thesis: verum

end;

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

F: rng (f +~ x,y) c= (rng f) \/ (rng ((x .--> y) * f)) by Th18;
rng (x .--> y) = {y} by FUNCOP_1:14;
then (rng f) \/ (rng ((x .--> y) * f)) c= (rng f) \/ {y} by RELAT_1:45, XBOOLE_1:9;
then G: rng (f +~ x,y) c= (rng f) \/ {y} by F, XBOOLE_1:1;
not x in rng (f +~ x,y) by S1, Tw2;
then (rng (f +~ x,y)) \ {x} = rng (f +~ x,y) by ZFMISC_1:65;
then rng (f +~ x,y) c= ((rng f) \/ {y}) \ {x} by G, XBOOLE_1:33;
hence rng (f +~ x,y) c= ((rng f) \ {x}) \/ {y} by S1, ZFMISC_1:147; :: thesis: verum

end;

end;