let K be Field; :: thesis: for i, n being Nat st 1 <= i & i <= n holds
(Base_FinSeq (K,n,i)) . i = 1. K
let i, n be Nat; :: thesis: ( 1 <= i & i <= n implies (Base_FinSeq (K,n,i)) . i = 1. K )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: (Base_FinSeq (K,n,i)) . i = 1. K
A2: len (n |-> (0. K)) = n by CARD_1:def 7;
len (Replace ((n |-> (0. K)),i,(1. K))) = len (n |-> (0. K)) by FINSEQ_7:5
.= n by CARD_1:def 7 ;
hence (Base_FinSeq (K,n,i)) . i = (Replace ((n |-> (0. K)),i,(1. K))) /. i by A1, FINSEQ_4:15
.= 1. K by A1, A2, FINSEQ_7:8 ;
:: thesis: verum