let K be Field; :: thesis: for i, j, n being Nat st 1 <= j & j <= n & i <> j holds
(Base_FinSeq K,n,i) . j = 0. K
let i, j, n be Nat; :: thesis: ( 1 <= j & j <= n & i <> j implies (Base_FinSeq K,n,i) . j = 0. K )
assume that
A1: ( 1 <= j & j <= n ) and
A2: i <> j ; :: thesis: (Base_FinSeq K,n,i) . j = 0. K
A3: j in Seg n by A1, FINSEQ_1:3;
A4: 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) . j = (Replace (n |-> (0. K)),i,(1. K)) /. j by A1, FINSEQ_4:24
.= (n |-> (0. K)) /. j by A1, A2, A4, FINSEQ_7:12
.= (n |-> (0. K)) . j by A1, A4, FINSEQ_4:24
.= 0. K by A3, FINSEQ_2:71 ;
:: thesis: verum