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