x = 0. X by STRUCT_0:def 12;
hence ||.x.|| is zero by Def6; :: thesis: verum