assume a *' is zero ; :: thesis: contradiction
then A1: a *' = 0. N ;
(a *') * a = (||.a.|| ^2) * (1. N) by Def3;
hence contradiction by A1, RLVECT_1:11; :: thesis: verum