theorem :: VALUED_1:17

for f1, f2 being complex-valued Function
for c being object holds (f1 /" f2) . c = (f1 . c) / (f2 . c)