let n, k 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;
assume not Solutions_of (0. K,n,k),B is empty ; :: thesis: B = 0. K,n,(width B)
then consider x being set such that
A1: x in Solutions_of (0. K,n,k),B by XBOOLE_0:def 1;
consider X being Matrix of K such that
A2: ( X = x & len X = width (0. K,n,k) & width X = width B & (0. K,n,k) * X = B ) by A1;
set ZERO = 0. K,n,(width B);
A3: ( len (0. K,n,k) = n & len (0. K,n,(width B)) = n ) by MATRIX_1:def 3;
then A4: ( len B = len (0. K,n,(width B)) & dom (0. K,n,k) = Seg n ) by A1, Th33, FINSEQ_1:def 3;
then reconsider B' = B as Matrix of n, width B,K by A3, MATRIX_2:7;

now

let i be Nat; :: thesis: ( 1 <= i & i <= n implies B . i = (0. K,n,(width B)) . i )
assume A5: ( 1 <= i & i <= n ) ; :: thesis: B . i = (0. K,n,(width B)) . i
i in NAT by ORDINAL1:def 13;
then A6: ( i in Seg n & n > 0 & width (0. K,n,k) = k ) by A5, MATRIX_1:24;
then Line (0. K,n,k),i = (0. K,n,k) . i by MATRIX_2:10
.= (width (0. K,n,k)) |-> (0. K) by A6, FINSEQ_2:71 ;
then (width B) |-> (0. K) = Line B,i by A1, A2, A4, A6, Th41
.= B' . i by A6, MATRIX_2:10 ;
hence B . i = (0. K,n,(width B)) . i by A6, FINSEQ_2:71; :: thesis: verum

end;

hence B = 0. K,n,(width B) by A3, A4, FINSEQ_1:18; :: thesis: verum