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 that
A1: n > 0 and
A2: not Solutions_of (0. K,n,0 ),(0. K,n,m) is empty ; :: thesis: m = 0
consider x being set such that
A3: x in Solutions_of (0. K,n,0 ),(0. K,n,m) by A2, XBOOLE_0:def 1;
A4: width (0. K,n,0 ) = 0 by A1, MATRIX_1:24;
ex X being Matrix of K st
( X = x & len X = width (0. K,n,0 ) & width X = width (0. K,n,m) & (0. K,n,0 ) * X = 0. K,n,m ) by A3;
hence 0 = width (0. K,n,m) by A4, MATRIX_1:def 4
.= m by A1, MATRIX_1:24 ;
:: thesis: verum