let K be Field; :: thesis: for n, i being Nat holds len (Base_FinSeq (K,n,i)) = n
let n, i be Nat; :: thesis: len (Base_FinSeq (K,n,i)) = n
len (Replace ((n |-> (0. K)),i,(1. K))) = len (n |-> (0. K)) by FINSEQ_7:7
.= n by FINSEQ_1:def 18 ;
hence len (Base_FinSeq (K,n,i)) = n ; :: thesis: verum