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