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 ;
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 ;
then A5: ((0. K) * M1) * (i,j) = (0. K) * (M1 * (i,j)) by ;
(0. (K,(len M1),(width M1))) * (i,j) = 0. K by ;
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 ; :: thesis: verum