simplify the proof of weqdirprodcomm in uu0

Definition weqdirprodcomm X Y : weq (dirprod X Y) (dirprod Y X).