for X, Y being set
for P being compatible PFUNC_DOMAIN of X,Y holds union P is PartFunc of X,Y