let i be Nat; :: thesis: for K being Field
for A, B, X 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 A, B, X 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 A, B, X 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 CARD_1:def 7;
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 :: thesis: for k being Nat st 1 <= k & k <= len (Line (B,i)) holds
((width B) |-> (0. K)) . k = (Line (B,i)) . k

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
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:87;
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:66
.= (0. K) * (Sum (Col (X,k))) by FVSUM_1:73
.= 0. K
.= ((width B) |-> (0. K)) . k by A8, FINSEQ_2:57 ;
hence ((width B) |-> (0. K)) . k = (Line (B,i)) . k by A8, MATRIX_0:def 7; :: thesis: verum

end;

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