theorem Th76: :: MATRIXR2:76

for n, i, j being Nat st 1 <= j & j <= n & i <> j holds
(Base_FinSeq (n,i)) . j = 0