:: deftheorem defines UnionSt TURING_1:def 22 :
for t1, t2 being TuringStr holds UnionSt (t1,t2) = [: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:];