let K be Field; :: thesis: for a being Element of K
for A, B being Matrix of K st a <> 0. K holds
Solutions_of A,B = Solutions_of (a * A),(a * B)
let a be Element of K; :: thesis: for A, B being Matrix of K st a <> 0. K holds
Solutions_of A,B = Solutions_of (a * A),(a * B)
let A, B be Matrix of K; :: thesis: ( a <> 0. K implies Solutions_of A,B = Solutions_of (a * A),(a * B) )
assume A1: a <> 0. K ; :: thesis: Solutions_of A,B = Solutions_of (a * A),(a * B)
thus Solutions_of A,B c= Solutions_of (a * A),(a * B) :: according to XBOOLE_0:def 10 :: thesis: Solutions_of (a * A),(a * B) c= Solutions_of A,B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of A,B or x in Solutions_of (a * A),(a * B) )
assume A2: x in Solutions_of A,B ; :: thesis: x in Solutions_of (a * A),(a * B)
ex X being Matrix of K st
( x = X & len X = width A & width X = width B & A * X = B ) by A2;
hence x in Solutions_of (a * A),(a * B) by A2, Th35; :: thesis: verum

end;

A3: (a " ) * (a * A) = ((a " ) * a) * A by Th2
.= (1_ K) * A by A1, VECTSP_1:def 22
.= A by Th2 ;
A4: (a " ) * (a * B) = ((a " ) * a) * B by Th2
.= (1_ K) * B by A1, VECTSP_1:def 22
.= B by Th2 ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of (a * A),(a * B) or x in Solutions_of A,B )
assume A5: x in Solutions_of (a * A),(a * B) ; :: thesis: x in Solutions_of A,B
ex X being Matrix of K st
( x = X & len X = width (a * A) & width X = width (a * B) & (a * A) * X = a * B ) by A5;
hence x in Solutions_of A,B by A5, A3, A4, Th35; :: thesis: verum