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;

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 A3: x in Solutions_of (a * A),(a * B) ; :: thesis: x in Solutions_of A,B
consider X being Matrix of K such that
A4: ( x = X & len X = width (a * A) & width X = width (a * B) ) and
(a * A) * X = a * B by A3;
A5: (a " ) * (a * A) = ((a " ) * a) * A by Th2
.= (1_ K) * A by A1, VECTSP_1:def 22
.= A by Th2 ;
(a " ) * (a * B) = ((a " ) * a) * B by Th2
.= (1_ K) * B by A1, VECTSP_1:def 22
.= B by Th2 ;
hence x in Solutions_of A,B by A3, A4, A5, Th35; :: thesis: verum