theorem Th24: :: TURING_1:24

for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T st t . h = s holds
Tape-Chg (t,h,s) = t