theorem Th27: :: MATRIX14:27

for n being Element of NAT
for K being Field
for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
(1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j