let f, f0, f1 be FinSequence of REAL ; :: thesis: ( f = f0 + f1 implies dom f = (dom f0) /\ (dom f1) )
[:(rng f0),(rng f1):] c= [:REAL,REAL:] by ZFMISC_1:119;
then A1: [:(rng f0),(rng f1):] c= dom addreal by FUNCT_2:def 1;
assume f = f0 + f1 ; :: thesis: dom f = (dom f0) /\ (dom f1)
hence dom f = (dom f0) /\ (dom f1) by A1, FUNCOP_1:84; :: thesis: verum