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});
thus rng (F | ((dom F) \ (F " {y}))) = (rng F) \ {y} :: thesis: for x being set st x <> y holds
(F | ((dom F) \ (F " {y}))) " {x} = F " {x}

proof

A1: (rng F) \ {y} c= rng (F | ((dom F) \ (F " {y})))

proof

let Fx be set ; :: according to TARSKI:def 3 :: thesis: ( not Fx in (rng F) \ {y} or Fx in rng (F | ((dom F) \ (F " {y}))) )
assume A2: Fx in (rng F) \ {y} ; :: thesis: Fx in rng (F | ((dom F) \ (F " {y})))
consider x being set such that
A3: ( x in dom F & F . x = Fx ) by A2, FUNCT_1:def 5;
not Fx in {y} by A2, XBOOLE_0:def 5;
then not x in F " {y} by A3, FUNCT_1:def 13;
then x in (dom F) \ (F " {y}) by A3, XBOOLE_0:def 5;
then x in (dom F) /\ ((dom F) \ (F " {y})) by XBOOLE_0:def 4;
then x in dom (F | ((dom F) \ (F " {y}))) by RELAT_1:90;
then ( (F | ((dom F) \ (F " {y}))) . x in rng (F | ((dom F) \ (F " {y}))) & (F | ((dom F) \ (F " {y}))) . x = F . x ) by FUNCT_1:70, FUNCT_1:def 5;
hence Fx in rng (F | ((dom F) \ (F " {y}))) by A3; :: thesis: verum

end;

rng (F | ((dom F) \ (F " {y}))) c= (rng F) \ {y}

proof

let Fx be set ; :: according to TARSKI:def 3 :: thesis: ( not Fx in rng (F | ((dom F) \ (F " {y}))) or Fx in (rng F) \ {y} )
assume A4: Fx in rng (F | ((dom F) \ (F " {y}))) ; :: thesis: Fx in (rng F) \ {y}
consider x being set such that
A5: ( x in dom (F | ((dom F) \ (F " {y}))) & Fx = (F | ((dom F) \ (F " {y}))) . x ) by A4, FUNCT_1:def 5;
x in (dom F) /\ ((dom F) \ (F " {y})) by A5, RELAT_1:90;
then x in ((dom F) /\ (dom F)) \ (F " {y}) by XBOOLE_1:49;
then ( x in dom F & not x in F " {y} ) by XBOOLE_0:def 5;
then ( F . x in rng F & not F . x in {y} ) by FUNCT_1:def 5, FUNCT_1:def 13;
then ( Fx in rng F & not Fx in {y} ) by A5, FUNCT_1:70;
hence Fx in (rng F) \ {y} by XBOOLE_0:def 5; :: thesis: verum

end;

hence rng (F | ((dom F) \ (F " {y}))) = (rng F) \ {y} by A1, XBOOLE_0:def 10; :: thesis: verum

end;

let x be set ; :: thesis: ( x <> y implies (F | ((dom F) \ (F " {y}))) " {x} = F " {x} )
assume A6: x <> y ; :: thesis: (F | ((dom F) \ (F " {y}))) " {x} = F " {x}

now

let z be set ; :: thesis: ( z in F " {x} implies z in (dom F) \ (F " {y}) )
assume A7: z in F " {x} ; :: thesis: z in (dom F) \ (F " {y})
A8: ( z in dom F & F . z in {x} ) by A7, FUNCT_1:def 13;
then F . z <> y by A6, TARSKI:def 1;
then not F . z in {y} by TARSKI:def 1;
then not z in F " {y} by FUNCT_1:def 13;
hence z in (dom F) \ (F " {y}) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

then F " {x} c= (dom F) \ (F " {y}) by TARSKI:def 3;
hence (F | ((dom F) \ (F " {y}))) " {x} = F " {x} by FUNCT_2:175; :: thesis: verum