for n being Nat
for A, B1, B2 being Matrix of n,REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds
( B1 = B2 & A is invertible )