theorem Th54: :: NUMBER15:54

for f being complex-valued FinSequence holds len (f ^2) = len f