theorem Th8: :: MATRIX_6:8

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