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) = () |-> (0. K) holds
Line (B,i) = () |-> (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) = () |-> (0. K) holds
Line (B,i) = () |-> (0. K)

let A, B, X be Matrix of K; :: thesis: ( X in Solutions_of (A,B) & i in dom A & Line (A,i) = () |-> (0. K) implies Line (B,i) = () |-> (0. K) )
assume that
A1: X in Solutions_of (A,B) and
A2: i in dom A and
A3: Line (A,i) = () |-> (0. K) ; :: thesis: Line (B,i) = () |-> (0. K)
set wB0 = () |-> (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
(() |-> (0. K)) . k = (Line (B,i)) . k
let k be Nat; :: thesis: ( 1 <= k & k <= len (Line (B,i)) implies (() |-> (0. K)) . k = (Line (B,i)) . k )
assume A7: ( 1 <= k & k <= len (Line (B,i)) ) ; :: thesis: (() |-> (0. K)) . k = (Line (B,i)) . k
A8: k in Seg () by A4, A7;
len A = len B by ;
then dom A = Seg (len B) by FINSEQ_1:def 3;
then i in dom B by ;
then [i,k] in Indices B by ;
then B * (i,k) = (Line (A,i)) "*" (Col (X,k)) by
.= Sum ((0. K) * (Col (X,k))) by
.= (0. K) * (Sum (Col (X,k))) by FVSUM_1:73
.= 0. K
.= (() |-> (0. K)) . k by ;
hence ((width B) |-> (0. K)) . k = (Line (B,i)) . k by ; :: thesis: verum
end;
len (() |-> (0. K)) = width B by CARD_1:def 7;
hence Line (B,i) = () |-> (0. K) by A4, A6; :: thesis: verum