theorem :: VALUED_2:86

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