let K be Field; :: thesis: for M being Matrix of K st - M = 0. (K,(len M),(width M)) holds

M = 0. (K,(len M),(width M))

let M be Matrix of K; :: thesis: ( - M = 0. (K,(len M),(width M)) implies M = 0. (K,(len M),(width M)) )

assume - M = 0. (K,(len M),(width M)) ; :: thesis: M = 0. (K,(len M),(width M))

then - (- M) = 0. (K,(len M),(width M)) by Th9;

hence M = 0. (K,(len M),(width M)) by Th1; :: thesis: verum

M = 0. (K,(len M),(width M))

let M be Matrix of K; :: thesis: ( - M = 0. (K,(len M),(width M)) implies M = 0. (K,(len M),(width M)) )

assume - M = 0. (K,(len M),(width M)) ; :: thesis: M = 0. (K,(len M),(width M))

then - (- M) = 0. (K,(len M),(width M)) by Th9;

hence M = 0. (K,(len M),(width M)) by Th1; :: thesis: verum