let f, g be Function; :: thesis: ( f tolerates g implies rng (f +* g) = (rng f) \/ (rng g) )

assume A1: f tolerates g ; :: thesis: rng (f +* g) = (rng f) \/ (rng g)

thus rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; :: according to XBOOLE_0:def 10 :: thesis: (rng f) \/ (rng g) c= rng (f +* g)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng f) \/ (rng g) or x in rng (f +* g) )

assume A2: x in (rng f) \/ (rng g) ; :: thesis: x in rng (f +* g)

A3: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) by Th12;

A4: rng g c= rng (f +* g) by FUNCT_4:18;

assume A1: f tolerates g ; :: thesis: rng (f +* g) = (rng f) \/ (rng g)

thus rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; :: according to XBOOLE_0:def 10 :: thesis: (rng f) \/ (rng g) c= rng (f +* g)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng f) \/ (rng g) or x in rng (f +* g) )

assume A2: x in (rng f) \/ (rng g) ; :: thesis: x in rng (f +* g)

A3: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) by Th12;

A4: rng g c= rng (f +* g) by FUNCT_4:18;

per cases
( x in rng g or not x in rng g )
;

end;

suppose A5:
not x in rng g
; :: thesis: x in rng (f +* g)

then
x in rng f
by A2, XBOOLE_0:def 3;

then consider a being object such that

A6: a in dom f and

A7: x = f . a by FUNCT_1:def 3;

then x in f .: ((dom f) \ (dom g)) by A7, FUNCT_1:def 6;

hence x in rng (f +* g) by A3, XBOOLE_0:def 3; :: thesis: verum

end;then consider a being object such that

A6: a in dom f and

A7: x = f . a by FUNCT_1:def 3;

now :: thesis: not a in dom g

then
a in (dom f) \ (dom g)
by A6, XBOOLE_0:def 5;assume A8:
a in dom g
; :: thesis: contradiction

x = (f +* g) . a by A1, A6, A7, FUNCT_4:15

.= g . a by A8, FUNCT_4:13 ;

hence contradiction by A5, A8, FUNCT_1:def 3; :: thesis: verum

end;x = (f +* g) . a by A1, A6, A7, FUNCT_4:15

.= g . a by A8, FUNCT_4:13 ;

hence contradiction by A5, A8, FUNCT_1:def 3; :: thesis: verum

then x in f .: ((dom f) \ (dom g)) by A7, FUNCT_1:def 6;

hence x in rng (f +* g) by A3, XBOOLE_0:def 3; :: thesis: verum