A: a <> 0. F ;
assume a " is zero ; :: thesis: contradiction
then 0. F = a * (a ")
.= 1. F by A, VECTSP_1:def 10 ;
hence contradiction ; :: thesis: verum