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)

.= (1_ K) * A by A1, VECTSP_1:def 10

.= A by Th2 ;

A4: (a ") * (a * B) = ((a ") * a) * B by Th2

.= (1_ K) * B by A1, VECTSP_1:def 10

.= B by Th2 ;

let x be object ; :: 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

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

A3: (a ") * (a * A) =
((a ") * a) * A
by Th2
let x be object ; :: 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;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

.= (1_ K) * A by A1, VECTSP_1:def 10

.= A by Th2 ;

A4: (a ") * (a * B) = ((a ") * a) * B by Th2

.= (1_ K) * B by A1, VECTSP_1:def 10

.= B by Th2 ;

let x be object ; :: 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