let n be Element of 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 A1: ( B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n ) ; :: thesis: ( B1 = B2 & A is invertible )
then A2: (B1 * A) * B2 = B2 by Th70;
A3: (B1 * A) * B2 = B1 * (A * B2) by Th28
.= B1 by A1, Th71 ;
hence B1 = B2 by A1, Th70; :: thesis: A is invertible
thus A is invertible by A1, A2, A3, Def5; :: thesis: verum