theorem Th17: :: BORSUK_7:18

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