theorem Th27: :: RFUNCT_1:27

for f1, f2 being complex-valued Function holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)