theorem :: MATRIX_6:9

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