let j, n, i be Nat; :: thesis: ( 1 <= j & j <= n & i <> j implies (Base_FinSeq n,i) . j = 0 )
assume that
A1: ( 1 <= j & j <= n ) and
A2: i <> j ; :: thesis: (Base_FinSeq n,i) . j = 0
A3: j in Seg n by A1, FINSEQ_1:3;
thus (Base_FinSeq n,i) . j = (n |-> 0 ) . j by A2, FUNCT_7:34
.= 0 by A3, FINSEQ_2:71 ; :: thesis: verum