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_0:def 2;
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_0: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:1;
hence ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) by A5; :: 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_0:21; :: thesis: verum