theorem Th29: :: GOBOARD7:29

for i being Nat
for f being non empty standard FinSequence of (TOP-REAL 2) st i in dom f & i + 1 in dom f holds
f /. i <> f /. (i + 1)