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