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}
rng (x .--> y) = rng {[x,y]} by FUNCT_4:82
.= {y} by RELAT_1:9 ;
hence rng (f +* (x .--> y)) c= (rng f) \/ {y} by FUNCT_4:17; :: thesis: verum