let a be non zero Element of F; :: thesis: a is unital
a <> 0. F ;
then a * (a ") = 1. F by VECTSP_1:def 10;
then a divides 1. F by GCD_1:def 1;
hence a is unital by GCD_1:def 20; :: thesis: verum