theorem Th27: :: COMPLSP2:33

for x being complex-valued FinSequence holds x + (0c (len x)) = x