theorem Th9: :: TURING_1:9

for T being TuringStr
for s being All-State of T holds (Computation s) . 1 = Following s