theorem :: MATRIX14:56
for n being Element of NAT
for K being Field
for A, B being Matrix of n,K st A * B = 1. (K,n) holds
( A is invertible & B is invertible )