x = 0. F by STRUCT_0:def 12;
hence x * y = x by Th3; :: thesis: verum