let x, y be set ; :: thesis: for f being Function st f is one-to-one & x in dom f holds
rng (f +* (x,y)) = ((rng f) \ {(f . x)}) \/ {y}
let f be Function; :: thesis: ( f is one-to-one & x in dom f implies rng (f +* (x,y)) = ((rng f) \ {(f . x)}) \/ {y} )
assume that
A1: f is one-to-one and
A2: x in dom f ; :: thesis: rng (f +* (x,y)) = ((rng f) \ {(f . x)}) \/ {y}
set xy = x .--> y;
( dom (x .--> y) = {x} & rng (x .--> y) = {y} ) by FUNCOP_1:8;
then rng (f +* (x .--> y)) = (f .: ((dom f) \ {x})) \/ {y} by FRECHET:12
.= ((f .: (dom f)) \ (f .: {x})) \/ {y} by A1, FUNCT_1:64
.= ((rng f) \ (Im (f,x))) \/ {y} by RELAT_1:113
.= ((rng f) \ {(f . x)}) \/ {y} by A2, FUNCT_1:59 ;
hence rng (f +* (x,y)) = ((rng f) \ {(f . x)}) \/ {y} by A2, FUNCT_7:def 3; :: thesis: verum