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) )
assume A1: len M1 > 0 ; :: thesis: (0. K) * M1 = 0. K,(len M1),(width M1)
A2: ( len ((0. K) * M1) = len M1 & width ((0. K) * M1) = width M1 ) by MATRIX_3:def 5;
A3: len (0. K,(len M1),(width M1)) = len M1 by MATRIX_1:def 3;
then A4: width (0. K,(len M1),(width M1)) = width M1 by A1, MATRIX_1:20;
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 A5: [i,j] in Indices (0. K,(len M1),(width M1)) ; :: thesis: ((0. K) * M1) * i,j = (0. K,(len M1),(width M1)) * i,j
then A6: (0. K,(len M1),(width M1)) * i,j = 0. K by MATRIX_3:3;
Indices (0. K,(len M1),(width M1)) = Indices M1 by A3, A4, MATRIX_4:55;
then ((0. K) * M1) * i,j = (0. K) * (M1 * i,j) by A5, MATRIX_3:def 5;
hence ((0. K) * M1) * i,j = (0. K,(len M1),(width M1)) * i,j by A6, VECTSP_1:36; :: thesis: verum

end;

hence (0. K) * M1 = 0. K,(len M1),(width M1) by A2, A3, A4, MATRIX_1:21; :: thesis: verum