let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng (f1 + f2) or y in RAT )
assume y in rng (f1 + f2) ; :: thesis: y in RAT
then consider x being object such that
A1: x in dom (f1 + f2) and
A2: (f1 + f2) . x = y by FUNCT_1:def 3;
(f1 + f2) . x = (f1 . x) + (f2 . x) by A1, Def1;
hence y in RAT by A2, RAT_1:def 2; :: thesis: verum