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 A2, RELAT_1:61;
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 A4, FUNCT_1:def 7;
then A5: not Fx in {y} by A2, A3, FUNCT_1:47;
F . x in rng F by A4, FUNCT_1:def 3;
then Fx in rng F by A2, A3, FUNCT_1:47;
hence Fx in (rng F) \ {y} by A5, XBOOLE_0:def 5; :: 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 A6, FUNCT_1:def 3;
not Fx in {y} by A6, XBOOLE_0:def 5;
then not x in F " {y} by A8, FUNCT_1:def 7;
then x in (dom F) \ (F " {y}) by A7, XBOOLE_0:def 5;
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 A8, A9, FUNCT_1:47; :: 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 A11, FUNCT_1:def 7;
then F . z <> y by A10, TARSKI:def 1;
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 A11, FUNCT_1:def 7;
hence z in (dom F) \ (F " {y}) by A12, XBOOLE_0:def 5; :: 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