let n, i be Nat; :: thesis: ( 1 <= i & i <= n implies (Base_FinSeq (n,i)) . i = 1 )
A1: len (n |-> 0) = n by CARD_1:def 7;
assume ( 1 <= i & i <= n ) ; :: thesis: (Base_FinSeq (n,i)) . i = 1
then i in dom (n |-> 0) by A1, FINSEQ_3:25;
hence (Base_FinSeq (n,i)) . i = 1 by FUNCT_7:31; :: thesis: verum