let B1, B2 be Matrix of n,REAL; :: thesis: ( B1 * A = 1_Rmatrix n & A * B1 = 1_Rmatrix n & B2 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n implies B1 = B2 )
assume that
B1 * A = 1_Rmatrix n and
A2: A * B1 = 1_Rmatrix n and
A3: B2 * A = 1_Rmatrix n and
A * B2 = 1_Rmatrix n ; :: thesis: B1 = B2
A4: ( len A = n & width A = n ) by MATRIX_0:24;
( len B1 = n & width B2 = n ) by MATRIX_0:24;
then (B2 * A) * B1 = B2 * (1_Rmatrix n) by A2, A4, MATRIX_3:33;
then B1 = B2 * (1_Rmatrix n) by A3, Th70;
hence B1 = B2 by Th71; :: thesis: verum