for K being Field
for n being Nat
for M1 being Matrix of n,K holds (- M1) @ = - (M1 @)