for X, X9, Y, Y9, Z, Z9 being set
for f being PartFunc of [:X,Y:],Z
for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]