theorem Th6: :: TOPREAL7:6

for f, g being FinSequence of REAL st ( len f = len g or dom f = dom g ) holds
( len (f + g) = len f & dom (f + g) = dom f )