theorem Th22: :: NUMBER14:22

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