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