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

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