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