let n be Nat; :: thesis: 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 )
let A, B1, B2 be Matrix of n,REAL; :: thesis: ( B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n implies ( B1 = B2 & A is invertible ) )
assume that
A1: B1 * A = 1_Rmatrix n and
A2: A * B2 = 1_Rmatrix n ; :: thesis: ( B1 = B2 & A is invertible )
A3: (B1 * A) * B2 = B1 * (A * B2) by Th28
.= B1 by A2, Th71 ;
hence B1 = B2 by A1, Th70; :: thesis: A is invertible
(B1 * A) * B2 = B2 by A1, Th70;
hence A is invertible by A1, A2, A3; :: thesis: verum