let n, i be Nat; :: thesis: len (Base_FinSeq n,i) = n
len ((n |-> 0 ) +* i,1) = len (n |-> 0 ) by FUNCT_7:99
.= n by FINSEQ_1:def 18 ;
hence len (Base_FinSeq n,i) = n ; :: thesis: verum