let K be Field; 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; 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; ( a <> 0. K implies Solutions_of (A,B) = Solutions_of ((a * A),(a * B)) )
assume A1:
a <> 0. K
; Solutions_of (A,B) = Solutions_of ((a * A),(a * B))
thus
Solutions_of (A,B) c= Solutions_of ((a * A),(a * B))
XBOOLE_0:def 10 Solutions_of ((a * A),(a * B)) c= Solutions_of (A,B)
A3: (a ") * (a * A) =
((a ") * a) * A
by Th2
.=
(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 ; TARSKI:def 3 ( 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))
; 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; verum