let x be set ; :: thesis: for F being Function st x in dom F holds
union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (F . x)
let F be Function; :: thesis: ( x in dom F implies union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (F . x) )
set d = (dom F) \ {x};
set Fd = F | ((dom F) \ {x});
A1: F | (dom F) = F ;
assume A2: x in dom F ; :: thesis: union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (F . x)
then ((dom F) \ {x}) \/ {x} = dom F by ZFMISC_1:116;
then F = (F | ((dom F) \ {x})) \/ (F | {x}) by A1, RELAT_1:78;
then A3: rng F = (rng (F | ((dom F) \ {x}))) \/ (rng (F | {x})) by RELAT_1:12;
Im (F,x) = {(F . x)} by A2, FUNCT_1:59;
then rng (F | {x}) = {(F . x)} by RELAT_1:115;
then union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (union {(F . x)}) by A3, ZFMISC_1:78;
hence union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (F . x) by ZFMISC_1:25; :: thesis: verum