let n, i, j 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;
thus (Base_FinSeq (n,i)) . j = (n |-> 0) . j by A2, FUNCT_7:32
.= 0 by A3, FINSEQ_2:57 ; :: thesis: verum