let F be Function; :: thesis: for y being set holds
( rng (F | ((dom F) \ (F " {y}))) = (rng F) \ {y} & ( for x being set st x <> y holds
(F | ((dom F) \ (F " {y}))) " {x} = F " {x} ) )

let y be set ; :: thesis: ( rng (F | ((dom F) \ (F " {y}))) = (rng F) \ {y} & ( for x being set st x <> y holds
(F | ((dom F) \ (F " {y}))) " {x} = F " {x} ) )

set D = (dom F) \ (F " {y});
A1: rng (F | ((dom F) \ (F " {y}))) c= (rng F) \ {y}
proof
let Fx be object ; :: according to TARSKI:def 3 :: thesis: ( not Fx in rng (F | ((dom F) \ (F " {y}))) or Fx in (rng F) \ {y} )
assume Fx in rng (F | ((dom F) \ (F " {y}))) ; :: thesis: Fx in (rng F) \ {y}
then consider x being object such that
A2: x in dom (F | ((dom F) \ (F " {y}))) and
A3: Fx = (F | ((dom F) \ (F " {y}))) . x by FUNCT_1:def 3;
A4: x in (dom F) /\ ((dom F) \ (F " {y})) by ;
then x in ((dom F) /\ (dom F)) \ (F " {y}) by XBOOLE_1:49;
then not x in F " {y} by XBOOLE_0:def 5;
then not F . x in {y} by ;
then A5: not Fx in {y} by ;
F . x in rng F by ;
then Fx in rng F by ;
hence Fx in (rng F) \ {y} by ; :: thesis: verum
end;
(rng F) \ {y} c= rng (F | ((dom F) \ (F " {y})))
proof
let Fx be object ; :: according to TARSKI:def 3 :: thesis: ( not Fx in (rng F) \ {y} or Fx in rng (F | ((dom F) \ (F " {y}))) )
assume A6: Fx in (rng F) \ {y} ; :: thesis: Fx in rng (F | ((dom F) \ (F " {y})))
consider x being object such that
A7: x in dom F and
A8: F . x = Fx by ;
not Fx in {y} by ;
then not x in F " {y} by ;
then x in (dom F) \ (F " {y}) by ;
then x in (dom F) /\ ((dom F) \ (F " {y})) by XBOOLE_0:def 4;
then A9: x in dom (F | ((dom F) \ (F " {y}))) by RELAT_1:61;
then (F | ((dom F) \ (F " {y}))) . x in rng (F | ((dom F) \ (F " {y}))) by FUNCT_1:def 3;
hence Fx in rng (F | ((dom F) \ (F " {y}))) by ; :: thesis: verum
end;
hence rng (F | ((dom F) \ (F " {y}))) = (rng F) \ {y} by A1; :: thesis: for x being set st x <> y holds
(F | ((dom F) \ (F " {y}))) " {x} = F " {x}

let x be set ; :: thesis: ( x <> y implies (F | ((dom F) \ (F " {y}))) " {x} = F " {x} )
assume A10: x <> y ; :: thesis: (F | ((dom F) \ (F " {y}))) " {x} = F " {x}
now :: thesis: for z being object st z in F " {x} holds
z in (dom F) \ (F " {y})
let z be object ; :: thesis: ( z in F " {x} implies z in (dom F) \ (F " {y}) )
assume A11: z in F " {x} ; :: thesis: z in (dom F) \ (F " {y})
F . z in {x} by ;
then F . z <> y by ;
then not F . z in {y} by TARSKI:def 1;
then A12: not z in F " {y} by FUNCT_1:def 7;
z in dom F by ;
hence z in (dom F) \ (F " {y}) by ; :: thesis: verum
end;
then F " {x} c= (dom F) \ (F " {y}) ;
hence (F | ((dom F) \ (F " {y}))) " {x} = F " {x} by FUNCT_2:98; :: thesis: verum