let A, B, x be set ; :: thesis: ( B <> {} implies rng ((id A) +* (B --> x)) = (A \ B) \/ {x} )
assume A1: B <> {} ; :: thesis: rng ((id A) +* (B --> x)) = (A \ B) \/ {x}
set f = (id A) +* (B --> x);
thus rng ((id A) +* (B --> x)) c= (A \ B) \/ {x} :: according to XBOOLE_0:def 10 :: thesis: (A \ B) \/ {x} c= rng ((id A) +* (B --> x))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((id A) +* (B --> x)) or y in (A \ B) \/ {x} )
assume y in rng ((id A) +* (B --> x)) ; :: thesis: y in (A \ B) \/ {x}
then consider x1 being set such that
A2: ( x1 in dom ((id A) +* (B --> x)) & y = ((id A) +* (B --> x)) . x1 ) by FUNCT_1:def 5;
A3: x1 in (dom (id A)) \/ (dom (B --> x)) by A2, FUNCT_4:def 1;

per cases ( x1 in dom (B --> x) or not x1 in dom (B --> x) ) ;

suppose A4: x1 in dom (B --> x) ; :: thesis: y in (A \ B) \/ {x}

then A5: ((id A) +* (B --> x)) . x1 = (B --> x) . x1 by A3, FUNCT_4:def 1;
x1 in B by A4;
then (B --> x) . x1 = x by FUNCOP_1:13;
then y in {x} by A2, A5, TARSKI:def 1;
hence y in (A \ B) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A6: not x1 in dom (B --> x) ; :: thesis: y in (A \ B) \/ {x}

then A7: ((id A) +* (B --> x)) . x1 = (id A) . x1 by A3, FUNCT_4:def 1;
A8: not x1 in B by A6, FUNCOP_1:19;
A9: x1 in dom (id A) by A3, A6, XBOOLE_0:def 3;
then x1 in A \ B by A8, XBOOLE_0:def 5;
then x1 in (A \ B) \/ {x} by XBOOLE_0:def 3;
hence y in (A \ B) \/ {x} by A2, A7, A9, FUNCT_1:35; :: thesis: verum

end;

end;

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (A \ B) \/ {x} or y in rng ((id A) +* (B --> x)) )
assume A10: y in (A \ B) \/ {x} ; :: thesis: y in rng ((id A) +* (B --> x))
A11: rng (B --> x) = {x} by A1, FUNCOP_1:14;
(id A) .: (A \ B) = A \ B by Th13;
then (id A) .: ((dom (id A)) \ B) = A \ B by FUNCT_1:34;
then (id A) .: ((dom (id A)) \ (dom (B --> x))) = A \ B by FUNCOP_1:19;
hence y in rng ((id A) +* (B --> x)) by A10, A11, Th12; :: thesis: verum