Definition. Write τX,Y[U;VZ] for

z[Z=z]τX,Y[U|z=z;V|Z=z]