len (Base_FinSeq (n,i)) = n by MATRIXR2:74;
hence Base_FinSeq (n,i) is Element of REAL n by FINSEQ_2:92; :: thesis: verum