theorem Th58: :: FUNCT_3:58

for X, Y, Z being set
for f being Function of X,Y
for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
<:f,g:> is Function of X,[:Y,Z:]