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;

A8: now :: thesis: for k being Nat st 1 <= k & k <= len B holds
(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;

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