theorem Th7: :: TOPREAL7:7

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 )