let X be RealNormSpace-Sequence; :: thesis: dom (carr X) = dom X
dom (carr X) = Seg (len (carr X)) by FINSEQ_1:def 3;
hence dom (carr X) = Seg (len X) by PRVECT_1:def 11
.= dom X by FINSEQ_1:def 3 ;
:: thesis: verum