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 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;
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 ; :: 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