theorem :: FUNCT_4:61

for X, X9, Y, Y9 being set
for D, D9 being non empty set
for f being Function of [:X,Y:],D
for g being Function of [:X9,Y9:],D9 holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:D,D9:] by Th60;