theorem Th26: :: MATRIX14:26

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