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

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