for n being Element of NAT
for K being Field
for A being Matrix of n,K holds
( ex B1 being Matrix of n,K st B1 * A = 1. (K,n) iff ex B2 being Matrix of n,K st A * B2 = 1. (K,n) )