theorem Th19: :: MATRIX14:19

for n being Element of NAT
for K being Field
for A being Matrix of n,K holds
( A is invertible iff ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) )