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