let F be Function; :: thesis: for x, y being object holds rng F c= (rng (F +* (x,y))) \/ {(F . x)}
let x, y be object ; :: thesis: rng F c= (rng (F +* (x,y))) \/ {(F . x)}
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng F or z in (rng (F +* (x,y))) \/ {(F . x)} )
assume z in rng F ; :: thesis: z in (rng (F +* (x,y))) \/ {(F . x)}
then consider e being object such that
A1: e in dom F and
A2: z = F . e by FUNCT_1:def 3;
A3: dom F = dom (F +* (x,y)) by Th29;

per cases ( e = x or e <> x ) ;

suppose e = x ; :: thesis: z in (rng (F +* (x,y))) \/ {(F . x)}

then z in {(F . x)} by A2, TARSKI:def 1;
hence z in (rng (F +* (x,y))) \/ {(F . x)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose e <> x ; :: thesis: z in (rng (F +* (x,y))) \/ {(F . x)}

then (F +* (x,y)) . e = F . e by Th31;
then z in rng (F +* (x,y)) by A1, A2, A3, FUNCT_1:3;
hence z in (rng (F +* (x,y))) \/ {(F . x)} by XBOOLE_0:def 3; :: thesis: verum

end;

end;