theorem :: MATRIX_6:11

for K being Field
for n being Nat holds ((1. (K,n)) @) ~ = 1. (K,n)