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