theorem :: TURING_1:47

for tm1, tm2 being TuringStr
for t being Tape of (tm1 ';' tm2) st the Symbols of tm1 = the Symbols of tm2 holds
( t is Tape of tm1 & t is Tape of tm2 )