:: deftheorem defines SecondTuringState TURING_1:def 26 :
for s, t being TuringStr
for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds SecondTuringState x = (x `1) `2 ;