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