let K be Field; :: thesis: for M being Matrix of st - M = 0. K,(len M),(width M) holds
M = 0. K,(len M),(width M)
let M be Matrix of ; :: 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