let GF be Field; :: thesis: - (1. GF) <> 0. GF
assume not - (1. GF) <> 0. GF ; :: thesis: contradiction
then 1. GF = - (0. GF) by RLVECT_1:17;
hence contradiction by RLVECT_1:12; :: thesis: verum