let K be Field; :: thesis: for a being Element of K

for A being Matrix of K holds Indices (a * A) = Indices A

let a be Element of K; :: thesis: for A being Matrix of K holds Indices (a * A) = Indices A

let A be Matrix of K; :: thesis: Indices (a * A) = Indices A

( len (a * A) = len A & width (a * A) = width A ) by MATRIX_3:def 5;

hence Indices (a * A) = Indices A by FINSEQ_3:29; :: thesis: verum

for A being Matrix of K holds Indices (a * A) = Indices A

let a be Element of K; :: thesis: for A being Matrix of K holds Indices (a * A) = Indices A

let A be Matrix of K; :: thesis: Indices (a * A) = Indices A

( len (a * A) = len A & width (a * A) = width A ) by MATRIX_3:def 5;

hence Indices (a * A) = Indices A by FINSEQ_3:29; :: thesis: verum