theorem SFX: :: RVSUM_4:21
for f being complex-valued XFinSequence
for x being Nat holds (Sequel f) . x = f . x