theorem Th87: :: VALUED_2:87

for X, X1, X2 being set
for Y, Y1, Y2 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds f <##> (f1 <++> f2) = (f <##> f1) <++> (f <##> f2)