theorem Th57: :: MATRIXJ1:57

for K being Field
for i being Element of NAT holds 1. (K,<*i*>) = <*(1. (K,i))*>