theorem Th26: :: TURING_1:26

for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T
for i being object holds
( (Tape-Chg (t,h,s)) . h = s & ( i <> h implies (Tape-Chg (t,h,s)) . i = t . i ) )