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