theorem Th20: :: VALUED_2:20
for g, h, k being complex-valued Function holds (g /" h) (#) k = (g (#) k) /" h