theorem Th18: :: BORSUK_7:19
for c being Complex
for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2)