x <> 0. X ;
then 0 <> ||.x.|| by NORMSP_0:def 5;
hence ||.x.|| is positive ; :: thesis: verum