let K be Field; :: thesis: for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds
Line A,i = (width A) |-> (0. K) ) holds
Space_of_Solutions_of A = Space_of_Solutions_of (Segm A,N,(Seg (width A)))
let A be Matrix of K; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds
Line A,i = (width A) |-> (0. K) ) holds
Space_of_Solutions_of A = Space_of_Solutions_of (Segm A,N,(Seg (width A)))
let N be finite without_zero Subset of NAT ; :: thesis: ( N c= dom A & not N is empty & width A > 0 & ( for i being Nat st i in (dom A) \ N holds
Line A,i = (width A) |-> (0. K) ) implies Space_of_Solutions_of A = Space_of_Solutions_of (Segm A,N,(Seg (width A))) )
assume that
A1: ( N c= dom A & not N is empty ) and
A2: width A > 0 and
A3: for i being Nat st i in (dom A) \ N holds
Line A,i = (width A) |-> (0. K) ; :: thesis: Space_of_Solutions_of A = Space_of_Solutions_of (Segm A,N,(Seg (width A)))
set L = (len A) |-> (0. K);
set C = ColVec2Mx ((len A) |-> (0. K));
A4: ( len ((len A) |-> (0. K)) = len A & len (ColVec2Mx ((len A) |-> (0. K))) = len ((len A) |-> (0. K)) & dom A = Seg (len A) ) by FINSEQ_1:def 3, FINSEQ_1:def 18, MATRIX_1:def 3;
then A5: ( dom (ColVec2Mx ((len A) |-> (0. K))) = dom A & ColVec2Mx ((len A) |-> (0. K)) = 0. K,(len A),1 ) by Th32, FINSEQ_3:31;
A6: Seg (len A) <> {} by A4, A1, XBOOLE_1:3;
then A7: ( width (ColVec2Mx ((len A) |-> (0. K))) = 1 & not dom A is empty ) by A4, Th26;
then A8: card (Seg (width (ColVec2Mx ((len A) |-> (0. K))))) = 1 by FINSEQ_1:78;

now

let i be Nat; :: thesis: ( i in (dom A) \ N implies ( Line A,i = (width A) |-> (0. K) & Line (ColVec2Mx ((len A) |-> (0. K))),i = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) ) )
assume A9: i in (dom A) \ N ; :: thesis: ( Line A,i = (width A) |-> (0. K) & Line (ColVec2Mx ((len A) |-> (0. K))),i = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) )
A10: i in dom A by A9, XBOOLE_0:def 5;
then Line (ColVec2Mx ((len A) |-> (0. K))),i = (ColVec2Mx ((len A) |-> (0. K))) . i by A4, MATRIX_2:10
.= ((len A) |-> ((width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K))) . i by A5, A6, Th26
.= (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) by A4, A10, FINSEQ_2:71 ;
hence ( Line A,i = (width A) |-> (0. K) & Line (ColVec2Mx ((len A) |-> (0. K))),i = (width (ColVec2Mx ((len A) |-> (0. K)))) |-> (0. K) ) by A9, A3; :: thesis: verum

end;

then A11: Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) = Solutions_of (Segm A,N,(Seg (width A))),(Segm (ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) by A1, A5, Th45;

now

let k, l be Nat; :: thesis: ( [k,l] in Indices (Segm (ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) implies (Segm (ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) * k,l = (0. K,(card N),1) * k,l )
assume A12: [k,l] in Indices (Segm (ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) ; :: thesis: (Segm (ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) * k,l = (0. K,(card N),1) * k,l
A13: Indices (Segm (ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) = Indices (0. K,(card N),1) by A8, MATRIX_1:27;
reconsider kk = k, ll = l as Element of NAT by ORDINAL1:def 13;
( [:N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))):] c= Indices (ColVec2Mx ((len A) |-> (0. K))) & rng (Sgm N) = N & rng (Sgm (Seg 1)) = Seg 1 ) by A1, A4, A5, FINSEQ_1:def 13, ZFMISC_1:118;
then A14: [((Sgm N) . kk),((Sgm (Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) . ll)] in Indices (ColVec2Mx ((len A) |-> (0. K))) by A7, A12, MATRIX13:17;
thus (Segm (ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) * k,l = (ColVec2Mx ((len A) |-> (0. K))) * ((Sgm N) . kk),((Sgm (Seg (width (ColVec2Mx ((len A) |-> (0. K)))))) . ll) by A12, MATRIX13:def 1
.= 0. K by A14, A5, MATRIX_3:3
.= (0. K,(card N),1) * k,l by A12, A13, MATRIX_3:3 ; :: thesis: verum

end;

then A15: Segm (ColVec2Mx ((len A) |-> (0. K))),N,(Seg (width (ColVec2Mx ((len A) |-> (0. K))))) = 0. K,(card N),1 by A8, MATRIX_1:28
.= ColVec2Mx ((card N) |-> (0. K)) by Th32 ;
set S = Segm A,N,(Seg (width A));
set SA = Space_of_Solutions_of A;
set SS = Space_of_Solutions_of (Segm A,N,(Seg (width A)));
card N <> 0 by A1;
then card N > 0 ;
then width (Segm A,N,(Seg (width A))) = card (Seg (width A)) by MATRIX_1:24;
then A16: ( len (Segm A,N,(Seg (width A))) = card N & width A = width (Segm A,N,(Seg (width A))) ) by FINSEQ_1:78, MATRIX_1:def 3;
then ( the carrier of (Space_of_Solutions_of A) = Solutions_of A,((len A) |-> (0. K)) & the carrier of (Space_of_Solutions_of (Segm A,N,(Seg (width A)))) = Solutions_of (Segm A,N,(Seg (width A))),((card N) |-> (0. K)) ) by A2, Def5;
hence Space_of_Solutions_of A = Space_of_Solutions_of (Segm A,N,(Seg (width A))) by A16, A11, A15, VECTSP_4:37; :: thesis: verum