let F be Function; :: thesis: for x, y being object holds rng (F +* (x,y)) c= (rng F) \/ {y}
let x, y be object ; :: thesis: rng (F +* (x,y)) c= (rng F) \/ {y}
A1: rng (x .--> y) = {y} by FUNCOP_1:8;

per cases ( x in dom F or not x in dom F ) ;

suppose x in dom F ; :: thesis: rng (F +* (x,y)) c= (rng F) \/ {y}

then F +* (x,y) = F +* (x .--> y) by Def2;
hence rng (F +* (x,y)) c= (rng F) \/ {y} by A1, FUNCT_4:17; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: rng (F +* (x,y)) c= (rng F) \/ {y}

then F +* (x,y) = F by Def2;
hence rng (F +* (x,y)) c= (rng F) \/ {y} by XBOOLE_1:7; :: thesis: verum

end;

end;