let K be Field; :: thesis: for a being Element of K
for X, A, B being Matrix of K st X in Solutions_of A,B holds
( a * X in Solutions_of A,(a * B) & X in Solutions_of (a * A),(a * B) )
let a be Element of K; :: thesis: for X, A, B being Matrix of K st X in Solutions_of A,B holds
( a * X in Solutions_of A,(a * B) & X in Solutions_of (a * A),(a * B) )
let X, A, B be Matrix of K; :: thesis: ( X in Solutions_of A,B implies ( a * X in Solutions_of A,(a * B) & X in Solutions_of (a * A),(a * B) ) )
assume X in Solutions_of A,B ; :: thesis: ( a * X in Solutions_of A,(a * B) & X in Solutions_of (a * A),(a * B) )
then consider X1 being Matrix of K such that
A1: ( X = X1 & len X1 = width A & width X1 = width B ) and
A2: A * X1 = B ;
A3: ( len (a * X) = width A & width (a * X) = width X1 & width (a * B) = width B & len (a * A) = len A & width (a * A) = width A ) by A1, MATRIX_3:def 5;
( A * (a * X) = a * (A * X) & (a * A) * X = a * (A * X) ) by A1, Th1, MATRIXR1:22;
hence ( a * X in Solutions_of A,(a * B) & X in Solutions_of (a * A),(a * B) ) by A1, A2, A3; :: thesis: verum