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