let k, n be Nat; :: thesis: for K being Field

for B being Matrix of K st not Solutions_of ((0. (K,n,k)),B) is empty holds

B = 0. (K,n,(width B))

let K be Field; :: thesis: for B being Matrix of K st not Solutions_of ((0. (K,n,k)),B) is empty holds

B = 0. (K,n,(width B))

let B be Matrix of K; :: thesis: ( not Solutions_of ((0. (K,n,k)),B) is empty implies B = 0. (K,n,(width B)) )

set A = 0. (K,n,k);

set ZERO = 0. (K,n,(width B));

assume not Solutions_of ((0. (K,n,k)),B) is empty ; :: thesis: B = 0. (K,n,(width B))

then consider x being object such that

A1: x in Solutions_of ((0. (K,n,k)),B) ;

A2: len (0. (K,n,k)) = n by MATRIX_0:def 2;

A3: dom (0. (K,n,k)) = Seg n ;

A4: len (0. (K,n,(width B))) = n by MATRIX_0:def 2;

then A5: len B = len (0. (K,n,(width B))) by A1, A2, Th33;

then reconsider B9 = B as Matrix of n, width B,K by A4, MATRIX_0:51;

A6: ex X being Matrix of K st

( X = x & len X = width (0. (K,n,k)) & width X = width B & (0. (K,n,k)) * X = B ) by A1;

for B being Matrix of K st not Solutions_of ((0. (K,n,k)),B) is empty holds

B = 0. (K,n,(width B))

let K be Field; :: thesis: for B being Matrix of K st not Solutions_of ((0. (K,n,k)),B) is empty holds

B = 0. (K,n,(width B))

let B be Matrix of K; :: thesis: ( not Solutions_of ((0. (K,n,k)),B) is empty implies B = 0. (K,n,(width B)) )

set A = 0. (K,n,k);

set ZERO = 0. (K,n,(width B));

assume not Solutions_of ((0. (K,n,k)),B) is empty ; :: thesis: B = 0. (K,n,(width B))

then consider x being object such that

A1: x in Solutions_of ((0. (K,n,k)),B) ;

A2: len (0. (K,n,k)) = n by MATRIX_0:def 2;

A3: dom (0. (K,n,k)) = Seg n ;

A4: len (0. (K,n,(width B))) = n by MATRIX_0:def 2;

then A5: len B = len (0. (K,n,(width B))) by A1, A2, Th33;

then reconsider B9 = B as Matrix of n, width B,K by A4, MATRIX_0:51;

A6: ex X being Matrix of K st

( X = x & len X = width (0. (K,n,k)) & width X = width B & (0. (K,n,k)) * X = B ) by A1;

now :: thesis: for i being Nat st 1 <= i & i <= n holds

B . i = (0. (K,n,(width B))) . i

hence
B = 0. (K,n,(width B))
by A4, A5; :: thesis: verumB . i = (0. (K,n,(width B))) . i

let i be Nat; :: thesis: ( 1 <= i & i <= n implies B . i = (0. (K,n,(width B))) . i )

assume A7: ( 1 <= i & i <= n ) ; :: thesis: B . i = (0. (K,n,(width B))) . i

A8: width (0. (K,n,k)) = k by A7, MATRIX_0:23;

A9: i in Seg n by A7;

then Line ((0. (K,n,k)),i) = (0. (K,n,k)) . i by MATRIX_0:52

.= (width (0. (K,n,k))) |-> (0. K) by A9, A8, FINSEQ_2:57 ;

then (width B) |-> (0. K) = Line (B,i) by A1, A6, A3, A9, Th41

.= B9 . i by A9, MATRIX_0:52 ;

hence B . i = (0. (K,n,(width B))) . i by A9, FINSEQ_2:57; :: thesis: verum

end;assume A7: ( 1 <= i & i <= n ) ; :: thesis: B . i = (0. (K,n,(width B))) . i

A8: width (0. (K,n,k)) = k by A7, MATRIX_0:23;

A9: i in Seg n by A7;

then Line ((0. (K,n,k)),i) = (0. (K,n,k)) . i by MATRIX_0:52

.= (width (0. (K,n,k))) |-> (0. K) by A9, A8, FINSEQ_2:57 ;

then (width B) |-> (0. K) = Line (B,i) by A1, A6, A3, A9, Th41

.= B9 . i by A9, MATRIX_0:52 ;

hence B . i = (0. (K,n,(width B))) . i by A9, FINSEQ_2:57; :: thesis: verum