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

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