consider M being Matrix of n,F_Real such that

A2: Det M = - (1. F_Real) and

A3: ( M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds

( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) ) by A1, Lm1;

Det M <> 0. F_Real by A2;

then M is invertible by LAPLACE:34;

hence ex b_{1} being invertible Matrix of n,F_Real st

( b_{1} * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b_{1} holds

( ( k = m & k <> i implies b_{1} * (k,k) = 1. F_Real ) & ( k <> m implies b_{1} * (k,m) = 0. F_Real ) ) ) )
by A3; :: thesis: verum

A2: Det M = - (1. F_Real) and

A3: ( M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds

( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) ) by A1, Lm1;

Det M <> 0. F_Real by A2;

then M is invertible by LAPLACE:34;

hence ex b

( b

( ( k = m & k <> i implies b