let a be Real; :: thesis: for A being Matrix of REAL holds Indices (a * A) = Indices A
let A be Matrix of REAL; :: thesis: Indices (a * A) = Indices A
( len A = len (a * A) & width (a * A) = width A ) by Th27;
hence Indices (a * A) = Indices A by MATRIX_4:55; :: thesis: verum