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 and
A3: Line A,i = (width A) |-> (0. K) ; :: thesis: Line B,i = (width B) |-> (0. K)
set wB0 = (width B) |-> (0. K);
set LB = Line B,i;
A4: len (Line B,i) = width B by FINSEQ_1:def 18;
A5: ex X1 being Matrix of K st
( X = X1 & len X1 = width A & width X1 = width B & A * X1 = B ) by A1;

A6: now

let k be Nat; :: thesis: ( 1 <= k & k <= len (Line B,i) implies ((width B) |-> (0. K)) . k = (Line B,i) . k )
assume A7: ( 1 <= k & k <= len (Line B,i) ) ; :: thesis: ((width B) |-> (0. K)) . k = (Line B,i) . k
k in NAT by ORDINAL1:def 13;
then A8: k in Seg (width B) by A4, A7;
len A = len B by A1, Th33;
then dom A = Seg (len B) by FINSEQ_1:def 3;
then i in dom B by A2, FINSEQ_1:def 3;
then [i,k] in Indices B by A8, ZFMISC_1:106;
then B * i,k = (Line A,i) "*" (Col X,k) by A5, MATRIX_3:def 4
.= Sum ((0. K) * (Col X,k)) by A3, A5, 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;

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