theorem SL: :: NEWTON04:28

for f being complex-valued FinSequence
for x being Complex holds f + x = f + ((len f) |-> x)