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 & 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 MATRIX_2:7;
the carrier of (Space_of_Solutions_of B) c= the carrier of (Space_of_Solutions_of AB)

proof

let x be set ; :: 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 A5: x in the carrier of (Space_of_Solutions_of B) ; :: thesis: x in the carrier of (Space_of_Solutions_of AB)
x in Solutions_of B,((len B) |-> (0. K)) by A5, A3, Def5;
then consider f being FinSequence of K such that
A6: ( f = x & ColVec2Mx f in Solutions_of B,(ColVec2Mx ((len B) |-> (0. K))) ) ;
consider X being Matrix of K such that
A7: ( X = ColVec2Mx f & len X = width B ) and
A8: width X = width (ColVec2Mx ((len B) |-> (0. K))) and
A9: B * X = ColVec2Mx ((len B) |-> (0. K)) by A6;
A10: ( ColVec2Mx ((len B) |-> (0. K)) = 0. K,(len B),1 & ColVec2Mx ((len AB) |-> (0. K)) = 0. K,(len A),1 ) by A4, Th32;

now

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 A11: ( Solutions_of AB,(ColVec2Mx ((len AB) |-> (0. K))) = {{} } & len X = 0 ) by Th51, A4, A7, A10, MATRIX_1:def 4;
then X = {} ;
hence X in Solutions_of AB,(ColVec2Mx ((len AB) |-> (0. K))) by A11, TARSKI:def 1; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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