theorem Th11: :: TURING_1:11

for i, j being Nat
for T being TuringStr
for s being All-State of T st i <= j & Following ((Computation s) . i) = (Computation s) . i holds
(Computation s) . j = (Computation s) . i