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) ) )
A1: ( width (a * B) = width B & width (a * A) = width A ) by MATRIX_3:def 5;
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
A2: ( X = X1 & len X1 = width A ) and
A3: ( width X1 = width B & A * X1 = B ) ;
A4: ( len (a * X) = width A & width (a * X) = width X1 ) by A2, MATRIX_3:def 5;
( A * (a * X) = a * (A * X) & (a * A) * X = a * (A * X) ) by A2, Th1, MATRIXR1:22;
hence ( a * X in Solutions_of A,(a * B) & X in Solutions_of (a * A),(a * B) ) by A2, A3, A4, A1; :: thesis: verum