theorem Th23: :: NUMBER14:23

for n being Nat
for a, b being object
for f being FinSequence st n in dom f holds
(<*a,b*> ^ f) . (n + 2) = f . n