let K be Field; :: thesis: for a being Element of K
for A, B, X 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 A, B, X 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, B, X 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