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:1;
A4: 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)) . j = (Replace ((n |-> (0. K)),i,(1. K))) /. j by A1, FINSEQ_4:15
.= (n |-> (0. K)) /. j by A1, A2, A4, FINSEQ_7:10
.= (n |-> (0. K)) . j by A1, A4, FINSEQ_4:15
.= 0. K by A3, FINSEQ_2:57 ;
:: thesis: verum