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 ;
hence a is unital ; :: thesis: verum