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