let m, n 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 object such that
A3: x in Solutions_of ((0. (K,n,0)),(0. (K,n,m))) by A2;
A4: width (0. (K,n,0)) = 0 by A1, MATRIX_0:23;
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_0:def 3
.= m by A1, MATRIX_0:23 ;
:: thesis: verum