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