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 () & 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 () & 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 () & 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 () 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 ()):] by FINSEQ_1:def 3;
then [k,i] in Indices B by ;
then A11: B * (k,i) = (Line (A,k)) "*" (Col (X1,i)) by
.= Sum ((0. K) * (Line (A,k))) by
.= (0. K) * (Sum (Line (A,k))) by FVSUM_1:73
.= 0. K
.= ((len B) |-> (0. K)) . k by ;
k in dom B by ;
hence (Col (B,i)) . k = ((len B) |-> (0. K)) . k by ; :: 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