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