let K be Field; :: thesis: for A, B being Matrix of K st width A = len B & ( width A = 0 implies len A = 0 ) & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B)
let A, B be Matrix of K; :: thesis: ( width A = len B & ( width A = 0 implies len A = 0 ) & ( width B = 0 implies len B = 0 ) implies Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) )
assume that
A1: width A = len B and
A2: ( width A = 0 implies len A = 0 ) and
A3: ( width B = 0 implies len B = 0 ) ; :: thesis: Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B)
set AB = A * B;
A4: len (A * B) = len A by A1, MATRIX_3:def 4;
A5: width (A * B) = width B by A1, MATRIX_3:def 4;
then reconsider AB = A * B as Matrix of len A, width B,K by A4, MATRIX_0:51;
the carrier of (Space_of_Solutions_of B) c= the carrier of (Space_of_Solutions_of AB)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Space_of_Solutions_of B) or x in the carrier of (Space_of_Solutions_of AB) )
assume x in the carrier of (Space_of_Solutions_of B) ; :: thesis: x in the carrier of (Space_of_Solutions_of AB)
then x in Solutions_of (B,((len B) |-> (0. K))) by A3, Def5;
then consider f being FinSequence of K such that
A6: f = x and
A7: ColVec2Mx f in Solutions_of (B,(ColVec2Mx ((len B) |-> (0. K)))) ;
consider X being Matrix of K such that
A8: X = ColVec2Mx f and
A9: len X = width B and
A10: width X = width (ColVec2Mx ((len B) |-> (0. K))) and
A11: B * X = ColVec2Mx ((len B) |-> (0. K)) by A7;
A12: ColVec2Mx ((len AB) |-> (0. K)) = 0. (K,(len A),1) by A4, Th32;
A13: ColVec2Mx ((len B) |-> (0. K)) = 0. (K,(len B),1) by Th32;

now :: thesis: X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K))))

per cases ( len A = 0 or len A <> 0 ) ;

suppose len A = 0 ; :: thesis: X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K))))

then ( Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K)))) = {{}} & X = {} ) by A4, A5, A9, A12, Th51, MATRIX_0:def 3;
hence X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K)))) by TARSKI:def 1; :: thesis: verum

end;

suppose A14: len A <> 0 ; :: thesis: X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K))))

then A15: width (ColVec2Mx ((len AB) |-> (0. K))) = 1 by A4, Th26
.= width (ColVec2Mx ((len B) |-> (0. K))) by A1, A2, A14, Th26 ;
ColVec2Mx ((len AB) |-> (0. K)) = A * (B * X) by A1, A2, A11, A13, A12, A14, MATRIXR2:18
.= AB * X by A1, A9, MATRIX_3:33 ;
hence X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K)))) by A5, A9, A10, A15; :: thesis: verum

end;

end;

end;

then f in Solutions_of (AB,((len AB) |-> (0. K))) by A8;
hence x in the carrier of (Space_of_Solutions_of AB) by A1, A2, A3, A4, A5, A6, Def5; :: thesis: verum

end;

hence Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) by A5, VECTSP_4:27; :: thesis: verum