theorem Th75: :: MATRIXR2:75

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