let K be Field; 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; ( 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
; (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
;
verum