theorem :: VALUED_1:18

for f being complex-valued Function
for c being object holds |.f.| . c = |.(f . c).|