let f be Real_Sequence; :: thesis: for n being Nat holds dom (FinSeq (f,n)) = Seg n

let n be Nat; :: thesis: dom (FinSeq (f,n)) = Seg n

dom f = NAT by FUNCT_2:def 1;

hence dom (FinSeq (f,n)) = Seg n by RELAT_1:62; :: thesis: verum

let n be Nat; :: thesis: dom (FinSeq (f,n)) = Seg n

dom f = NAT by FUNCT_2:def 1;

hence dom (FinSeq (f,n)) = Seg n by RELAT_1:62; :: thesis: verum