let n be Nat; :: thesis: for K being Field
for A being Matrix of n,n,K
for B being Matrix of K st Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
let K be Field; :: thesis: for A being Matrix of n,n,K
for B being Matrix of K st Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
let A be Matrix of n,n,K; :: thesis: for B being Matrix of K st Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
let B be Matrix of K; :: thesis: ( Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) implies Space_of_Solutions_of B = Space_of_Solutions_of (A * B) )
assume that
A1: ( Det A <> 0. K & width A = len B ) and
A2: ( width B = 0 implies len B = 0 ) ; :: thesis: Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
set AB = A * B;
A3: ( len A = n & width A = n ) by MATRIX_1:25;
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 n, width B,K by A3, MATRIX_2:7;
A5: ( width A = 0 implies len A = 0 ) by A3;
A6: the carrier of (Space_of_Solutions_of AB) c= the carrier of (Space_of_Solutions_of B)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Space_of_Solutions_of AB) or x in the carrier of (Space_of_Solutions_of B) )
assume A7: x in the carrier of (Space_of_Solutions_of AB) ; :: thesis: x in the carrier of (Space_of_Solutions_of B)
x in Solutions_of AB,((len AB) |-> (0. K)) by A1, A2, A7, A4, A3, Def5;
then consider f being FinSequence of K such that
A8: ( f = x & ColVec2Mx f in Solutions_of AB,(ColVec2Mx ((len AB) |-> (0. K))) ) ;
consider X being Matrix of K such that
A9: ( X = ColVec2Mx f & len X = width AB ) and
A10: width X = width (ColVec2Mx ((len AB) |-> (0. K))) and
A11: AB * X = ColVec2Mx ((len AB) |-> (0. K)) by A8;
set BX = B * X;
A is invertible by A1, LAPLACE:34;
then A is_reverse_of A ~ by MATRIX_6:def 4;
then A12: 1. K,n = (A ~ ) * A by MATRIX_6:def 2;
A13: ( len (A ~ ) = n & width (A ~ ) = n ) by MATRIX_1:25;
A14: len (B * X) = len B by A4, A9, MATRIX_3:def 4;
then A15: B * X = (1. K,n) * (B * X) by A1, A3, MATRIXR2:68
.= (A ~ ) * (A * (B * X)) by A1, A3, A12, A13, A14, MATRIX_3:35
.= (A ~ ) * (ColVec2Mx ((len AB) |-> (0. K))) by A1, A4, A9, A11, MATRIX_3:35
.= (A ~ ) * (0. K,(len AB),1) by Th32 ;

now

per cases ( n = 0 or n > 0 ) ;

suppose A16: n = 0 ; :: thesis: B * X = 0. K,(len AB),1

len (0. K,(len AB),1) = width (A ~ ) by A3, A4, A13, MATRIX_1:def 3;
then ( B * X = {} & 0. K,(len AB),1 = {} ) by A1, A3, A13, A14, A16;
hence B * X = 0. K,(len AB),1 ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: B * X = 0. K,(len AB),1

hence B * X = 0. K,(len AB),1 by A3, A4, A13, A15, MATRIXR2:18; :: thesis: verum

end;

end;

end;

then B * X = ColVec2Mx ((len AB) |-> (0. K)) by Th32;
then ColVec2Mx f in Solutions_of B,(ColVec2Mx ((len B) |-> (0. K))) by A1, A3, A4, A9, A10;
then f in Solutions_of B,((len B) |-> (0. K)) ;
hence x in the carrier of (Space_of_Solutions_of B) by A2, A8, Def5; :: thesis: verum

end;

Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) by A1, A2, A5, Th72;
then the carrier of (Space_of_Solutions_of B) c= the carrier of (Space_of_Solutions_of (A * B)) by VECTSP_4:def 2;
then the carrier of (Space_of_Solutions_of B) = the carrier of (Space_of_Solutions_of (A * B)) by A6, XBOOLE_0:def 10;
hence Space_of_Solutions_of B = Space_of_Solutions_of (A * B) by A4, VECTSP_4:37; :: thesis: verum