simplify the proof of weqdirprodcomm in uu0, part 2