let i be Nat; :: thesis: for K being Field
for X, A, B being Matrix of K st X in Solutions_of A,B & i in dom A & Line A,i = (width A) |-> (0. K) holds
Line B,i = (width B) |-> (0. K)
let K be Field; :: thesis: for X, A, B being Matrix of K st X in Solutions_of A,B & i in dom A & Line A,i = (width A) |-> (0. K) holds
Line B,i = (width B) |-> (0. K)
let X, A, B be Matrix of K; :: thesis: ( X in Solutions_of A,B & i in dom A & Line A,i = (width A) |-> (0. K) implies Line B,i = (width B) |-> (0. K) )
assume that
A1: X in Solutions_of A,B and
A2: ( i in dom A & Line A,i = (width A) |-> (0. K) ) ; :: thesis: Line B,i = (width B) |-> (0. K)
consider X1 being Matrix of K such that
A3: ( X = X1 & len X1 = width A & width X1 = width B ) and
A4: A * X1 = B by A1;
set LB = Line B,i;
set wB0 = (width B) |-> (0. K);
A5: ( len (Line B,i) = width B & len ((width B) |-> (0. K)) = width B ) by FINSEQ_1:def 18;

now

let k be Nat; :: thesis: ( 1 <= k & k <= len (Line B,i) implies ((width B) |-> (0. K)) . k = (Line B,i) . k )
assume A6: ( 1 <= k & k <= len (Line B,i) ) ; :: thesis: ((width B) |-> (0. K)) . k = (Line B,i) . k
A7: k in NAT by ORDINAL1:def 13;
len A = len B by Th33, A1;
then dom A = Seg (len B) by FINSEQ_1:def 3;
then A8: ( k in Seg (width B) & i in dom B ) by A6, A5, A2, A7, FINSEQ_1:def 3;
then [i,k] in Indices B by ZFMISC_1:106;
then B * i,k = (Line A,i) "*" (Col X,k) by A3, A4, MATRIX_3:def 4
.= Sum ((0. K) * (Col X,k)) by A2, A3, FVSUM_1:80
.= (0. K) * (Sum (Col X,k)) by FVSUM_1:92
.= 0. K by VECTSP_1:36
.= ((width B) |-> (0. K)) . k by A8, FINSEQ_2:71 ;
hence ((width B) |-> (0. K)) . k = (Line B,i) . k by A8, MATRIX_1:def 8; :: thesis: verum

end;

hence Line B,i = (width B) |-> (0. K) by A5, FINSEQ_1:18; :: thesis: verum