let A1, A2 be invertible Matrix of n,F_Real; :: thesis: ( A1 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices A1 holds
( ( k = m & k <> i implies A1 * (k,k) = 1. F_Real ) & ( k <> m implies A1 * (k,m) = 0. F_Real ) ) ) & A2 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices A2 holds
( ( k = m & k <> i implies A2 * (k,k) = 1. F_Real ) & ( k <> m implies A2 * (k,m) = 0. F_Real ) ) ) implies A1 = A2 )
assume that
A4: A1 * (i,i) = - (1. F_Real) and
A5: for k, m being Nat st [k,m] in Indices A1 holds
( ( k = m & k <> i implies A1 * (k,k) = 1. F_Real ) & ( k <> m implies A1 * (k,m) = 0. F_Real ) ) and
A6: A2 * (i,i) = - (1. F_Real) and
A7: for k, m being Nat st [k,m] in Indices A2 holds
( ( k = m & k <> i implies A2 * (k,k) = 1. F_Real ) & ( k <> m implies A2 * (k,m) = 0. F_Real ) ) ; :: thesis: A1 = A2
for k, m being Nat st [k,m] in Indices A1 holds
A1 * (k,m) = A2 * (k,m)

proof

let k, m be Nat; :: thesis: ( [k,m] in Indices A1 implies A1 * (k,m) = A2 * (k,m) )
assume A8: [k,m] in Indices A1 ; :: thesis: A1 * (k,m) = A2 * (k,m)
then A9: [k,m] in Indices A2 by MATRIX_0:26;

per cases ( k <> m or ( k = m & k <> i ) or ( k = m & k = i ) ) ;

suppose A10: k <> m ; :: thesis: A1 * (k,m) = A2 * (k,m)

then A1 * (k,m) = 0. F_Real by A5, A8;
hence A1 * (k,m) = A2 * (k,m) by A7, A9, A10; :: thesis: verum

end;

suppose A11: ( k = m & k <> i ) ; :: thesis: A1 * (k,m) = A2 * (k,m)

then A1 * (k,m) = 1. F_Real by A5, A8;
hence A1 * (k,m) = A2 * (k,m) by A7, A9, A11; :: thesis: verum

end;

suppose ( k = m & k = i ) ; :: thesis: A1 * (k,m) = A2 * (k,m)

hence A1 * (k,m) = A2 * (k,m) by A4, A6; :: thesis: verum

end;

end;

end;

hence A1 = A2 by MATRIX_0:27; :: thesis: verum