let K be Field; :: thesis: for M1 being Matrix of K st len M1 > 0 holds
(0. K) * M1 = 0. K,(len M1),(width M1)
let M1 be Matrix of K; :: thesis: ( len M1 > 0 implies (0. K) * M1 = 0. K,(len M1),(width M1) )
A1: len (0. K,(len M1),(width M1)) = len M1 by MATRIX_1:def 3;
assume len M1 > 0 ; :: thesis: (0. K) * M1 = 0. K,(len M1),(width M1)
then A2: width (0. K,(len M1),(width M1)) = width M1 by A1, MATRIX_1:20;
A3: for i, j being Nat st [i,j] in Indices (0. K,(len M1),(width M1)) holds
((0. K) * M1) * i,j = (0. K,(len M1),(width M1)) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (0. K,(len M1),(width M1)) implies ((0. K) * M1) * i,j = (0. K,(len M1),(width M1)) * i,j )
assume A4: [i,j] in Indices (0. K,(len M1),(width M1)) ; :: thesis: ((0. K) * M1) * i,j = (0. K,(len M1),(width M1)) * i,j
Indices (0. K,(len M1),(width M1)) = Indices M1 by A1, A2, MATRIX_4:55;
then A5: ((0. K) * M1) * i,j = (0. K) * (M1 * i,j) by A4, MATRIX_3:def 5;
(0. K,(len M1),(width M1)) * i,j = 0. K by A4, MATRIX_3:3;
hence ((0. K) * M1) * i,j = (0. K,(len M1),(width M1)) * i,j by A5, VECTSP_1:36; :: thesis: verum

end;

( len ((0. K) * M1) = len M1 & width ((0. K) * M1) = width M1 ) by MATRIX_3:def 5;
hence (0. K) * M1 = 0. K,(len M1),(width M1) by A1, A2, A3, MATRIX_1:21; :: thesis: verum