let n, m be Nat; :: thesis: for K being Field st n > 0 & not Solutions_of (0. K,n,0 ),(0. K,n,m) is empty holds
m = 0
let K be Field; :: thesis: ( n > 0 & not Solutions_of (0. K,n,0 ),(0. K,n,m) is empty implies m = 0 )
assume A1: ( n > 0 & not Solutions_of (0. K,n,0 ),(0. K,n,m) is empty ) ; :: thesis: m = 0
then consider x being set such that
A2: x in Solutions_of (0. K,n,0 ),(0. K,n,m) by XBOOLE_0:def 1;
consider X being Matrix of K such that
A3: ( X = x & len X = width (0. K,n,0 ) ) and
A4: width X = width (0. K,n,m) and
(0. K,n,0 ) * X = 0. K,n,m by A2;
width (0. K,n,0 ) = 0 by A1, MATRIX_1:24;
hence 0 = width (0. K,n,m) by A4, A3, MATRIX_1:def 4
.= m by A1, MATRIX_1:24 ;
:: thesis: verum