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;

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

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

len ((width B) |-> (0. K)) = width B
by CARD_1:def 7;((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;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

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