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