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_2:def 4

.= dom X by FINSEQ_1:def 3 ;

:: thesis: verum

dom (carr X) = Seg (len (carr X)) by FINSEQ_1:def 3;

hence dom (carr X) = Seg (len X) by PRVECT_2:def 4

.= dom X by FINSEQ_1:def 3 ;

:: thesis: verum