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