theorem Th1: :: NOMIN_1:1

for x being object
for n being Nat
for f being FinSequence st n in dom f holds
(<*x*> ^ f) . (n + 1) = f . n