theorem SL: :: NEWTON04:28

for f being FinSequence of COMPLEX
for x being Complex holds f + x = f + ((len f) |-> x)