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}

(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}

hence (F | ((dom F) \ (F " {y}))) " {x} = F " {x} by FUNCT_2:98; :: thesis: verum

( 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

(rng F) \ {y} c= rng (F | ((dom F) \ (F " {y})))
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;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

proof

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

(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})

then
F " {x} c= (dom F) \ (F " {y})
;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;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

hence (F | ((dom F) \ (F " {y}))) " {x} = F " {x} by FUNCT_2:98; :: thesis: verum