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 FINSEQ_1:def 18;
len (Replace (n |-> (0. K)),i,(1. K)) = len (n |-> (0. K)) by FINSEQ_7:7
.= n by FINSEQ_1:def 18 ;
hence (Base_FinSeq K,n,i) . i = (Replace (n |-> (0. K)),i,(1. K)) /. i by A1, FINSEQ_4:24
.= 1. K by A1, A2, FINSEQ_7:10 ;
:: thesis: verum