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:
set AB = A * B;
A4: len (A * B) = len A by ;
A5: width (A * B) = width B by ;
then reconsider AB = A * B as Matrix of len A, width B,K by ;
the carrier of c= the carrier of
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of or x in the carrier of )
assume x in the carrier of ; :: thesis: x in the carrier of
then x in Solutions_of (B,((len B) |-> (0. K))) by ;
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 ;
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 ;
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
.= width (ColVec2Mx ((len B) |-> (0. K))) by A1, A2, A14, Th26 ;
ColVec2Mx ((len AB) |-> (0. K)) = A * (B * X) by
.= AB * X by ;
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 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 ; :: thesis: verum