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)
consider X1 being Matrix of K such that
A4: ( X = X1 & len X1 = width A & width X1 = width B ) and
A5: A * X1 = B by A1;
set LB0 = (len B) |-> (0. K);
A6: ( len (Col B,i) = len B & len ((len B) |-> (0. K)) = len B ) by FINSEQ_1:def 18;

now

let k be Nat; :: thesis: ( 1 <= k & k <= len B implies (Col B,i) . k = ((len B) |-> (0. K)) . k )
assume A7: ( 1 <= k & k <= len B ) ; :: thesis: (Col B,i) . k = ((len B) |-> (0. K)) . k
k in NAT by ORDINAL1:def 13;
then A8: ( k in Seg (len B) & Indices B = [:(Seg (len B)),(Seg (width B)):] ) by A7, FINSEQ_1:def 3;
then ( [k,i] in Indices B & width A = len X1 ) by A2, A4, ZFMISC_1:106;
then A9: B * k,i = (Line A,k) "*" (Col X1,i) by A5, MATRIX_3:def 4
.= Sum ((0. K) * (Line A,k)) by A3, A4, 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 A8, FINSEQ_2:71 ;
k in dom B by A8, FINSEQ_1:def 3;
hence (Col B,i) . k = ((len B) |-> (0. K)) . k by A9, MATRIX_1:def 9; :: thesis: verum

end;

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