theorem :: TOPREALC:10

for c being Complex
for f being complex-valued Function holds (f (/) c) ^2 = (f ^2) (/) (c ^2)