I guess that "having a sharp look" means how to do that manually/intuitively. Well, I would first check which states are compatible in the sense that they agree on the variables that they know. The two structures share variable x, and therefore we can pair the states

- ({},{}); ({},{q})
- ({x},{x}); ({x},{q;x})
- ({x;y},{x}); ({x;y},{q;x})

The union of these state pairs will give the product states. After this, we have to determine the transitions in that we have to check for each pair of pairs (s1,s2) and (s1',s2') whether we have s1->s1' and s2->s2'. If so, we have a transition, otherwise, we don't. Instead of inspecting all 36 pairs in the above case, we may also inspect all transitions s1->s1' of K1 and check for which states (s1,s2) there is a state (s1',s2') with s2->s2'.