let A, B, x be set ; :: thesis: ( B <> {} implies rng ((id A) +* (B --> x)) = (A \ B) \/ {x} )
set f = (id A) +* (B --> x);
assume B <> {} ; :: thesis: rng ((id A) +* (B --> x)) = (A \ B) \/ {x}
then A1: rng (B --> x) = {x} by FUNCOP_1:8;
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 object ; :: 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 object such that
A2: x1 in dom ((id A) +* (B --> x)) and
A3: y = ((id A) +* (B --> x)) . x1 by FUNCT_1:def 3;
A4: 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 x1 in dom (B --> x) ; :: thesis: y in (A \ B) \/ {x}

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

end;

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

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

end;

end;

end;

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