theorem DCARXX: :: LOPBAN11:4

for X being RealNormSpace-Sequence holds dom (carr X) = dom X