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 Seg (width X) & Col (X,i) = (len X) |-> (0. K) holds

Col (B,i) = (len 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 Seg (width X) & Col (X,i) = (len X) |-> (0. K) holds

Col (B,i) = (len B) |-> (0. K)

let A, B, X be Matrix of K; :: thesis: ( X in Solutions_of (A,B) & i in Seg (width X) & Col (X,i) = (len X) |-> (0. K) implies Col (B,i) = (len B) |-> (0. K) )

assume that

A1: X in Solutions_of (A,B) and

A2: i in Seg (width X) and

A3: Col (X,i) = (len X) |-> (0. K) ; :: thesis: Col (B,i) = (len B) |-> (0. K)

set LB0 = (len B) |-> (0. K);

consider X1 being Matrix of K such that

A4: X = X1 and

A5: len X1 = width A and

A6: width X1 = width B and

A7: A * X1 = B by A1;

hence Col (B,i) = (len B) |-> (0. K) by A8; :: thesis: verum

for A, B, X being Matrix of K st X in Solutions_of (A,B) & i in Seg (width X) & Col (X,i) = (len X) |-> (0. K) holds

Col (B,i) = (len 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 Seg (width X) & Col (X,i) = (len X) |-> (0. K) holds

Col (B,i) = (len B) |-> (0. K)

let A, B, X be Matrix of K; :: thesis: ( X in Solutions_of (A,B) & i in Seg (width X) & Col (X,i) = (len X) |-> (0. K) implies Col (B,i) = (len B) |-> (0. K) )

assume that

A1: X in Solutions_of (A,B) and

A2: i in Seg (width X) and

A3: Col (X,i) = (len X) |-> (0. K) ; :: thesis: Col (B,i) = (len B) |-> (0. K)

set LB0 = (len B) |-> (0. K);

consider X1 being Matrix of K such that

A4: X = X1 and

A5: len X1 = width A and

A6: width X1 = width B and

A7: A * X1 = B by A1;

A8: now :: thesis: for k being Nat st 1 <= k & k <= len B holds

(Col (B,i)) . k = ((len B) |-> (0. K)) . k

( len (Col (B,i)) = len B & len ((len B) |-> (0. K)) = len B )
by CARD_1:def 7;(Col (B,i)) . k = ((len B) |-> (0. K)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len B implies (Col (B,i)) . k = ((len B) |-> (0. K)) . k )

assume A9: ( 1 <= k & k <= len B ) ; :: thesis: (Col (B,i)) . k = ((len B) |-> (0. K)) . k

A10: k in Seg (len B) by A9;

Indices B = [:(Seg (len B)),(Seg (width B)):] by FINSEQ_1:def 3;

then [k,i] in Indices B by A2, A4, A6, A10, ZFMISC_1:87;

then A11: B * (k,i) = (Line (A,k)) "*" (Col (X1,i)) by A5, A7, MATRIX_3:def 4

.= Sum ((0. K) * (Line (A,k))) by A3, A4, A5, FVSUM_1:66

.= (0. K) * (Sum (Line (A,k))) by FVSUM_1:73

.= 0. K

.= ((len B) |-> (0. K)) . k by A10, FINSEQ_2:57 ;

k in dom B by A10, FINSEQ_1:def 3;

hence (Col (B,i)) . k = ((len B) |-> (0. K)) . k by A11, MATRIX_0:def 8; :: thesis: verum

end;assume A9: ( 1 <= k & k <= len B ) ; :: thesis: (Col (B,i)) . k = ((len B) |-> (0. K)) . k

A10: k in Seg (len B) by A9;

Indices B = [:(Seg (len B)),(Seg (width B)):] by FINSEQ_1:def 3;

then [k,i] in Indices B by A2, A4, A6, A10, ZFMISC_1:87;

then A11: B * (k,i) = (Line (A,k)) "*" (Col (X1,i)) by A5, A7, MATRIX_3:def 4

.= Sum ((0. K) * (Line (A,k))) by A3, A4, A5, FVSUM_1:66

.= (0. K) * (Sum (Line (A,k))) by FVSUM_1:73

.= 0. K

.= ((len B) |-> (0. K)) . k by A10, FINSEQ_2:57 ;

k in dom B by A10, FINSEQ_1:def 3;

hence (Col (B,i)) . k = ((len B) |-> (0. K)) . k by A11, MATRIX_0:def 8; :: thesis: verum

hence Col (B,i) = (len B) |-> (0. K) by A8; :: thesis: verum