let k, n be Nat; 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; 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; ( 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
; 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 for i being Nat st 1 <= i & i <= n holds
B . i = (0. (K,n,(width B))) . ilet i be
Nat;
( 1 <= i & i <= n implies B . i = (0. (K,n,(width B))) . i )assume A7:
( 1
<= i &
i <= n )
;
B . i = (0. (K,n,(width B))) . iA8:
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;
verum end;
hence
B = 0. (K,n,(width B))
by A4, A5; verum