for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is invertible iff Det M <> 0. K )