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 A1: ( f is one-to-one & 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:14, FUNCOP_1:19;
then rng (f +* (x .--> y)) = (f .: ((dom f) \ {x})) \/ {y} by FRECHET:12
.= ((f .: (dom f)) \ (f .: {x})) \/ {y} by A1, FUNCT_1:123
.= ((rng f) \ (Im f,x)) \/ {y} by RELAT_1:146
.= ((rng f) \ {(f . x)}) \/ {y} by A1, FUNCT_1:117 ;
hence rng (f +* x,y) = ((rng f) \ {(f . x)}) \/ {y} by A1, FUNCT_7:def 3; :: thesis: verum