theorem RXF: :: NUMERAL3:65

for n being Nat
for f being b₁ + 1 -element complex-valued XFinSequence holds f = ((f | n) ^ <%0%>) + ((n --> 0) ^ <%(f . n)%>)