let i be Nat; :: thesis: for K being Field
for X, A, B 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 X, A, B 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 X, A, B 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

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
k in NAT by ORDINAL1:def 13;
then 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:106;
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:80
.= (0. K) * (Sum (Line A,k)) by FVSUM_1:92
.= 0. K by VECTSP_1:36
.= ((len B) |-> (0. K)) . k by A10, FINSEQ_2:71 ;
k in dom B by A10, FINSEQ_1:def 3;
hence (Col B,i) . k = ((len B) |-> (0. K)) . k by A11, MATRIX_1:def 9; :: thesis: verum

end;

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