for s, t being TuringStr
for x being State of t holds [ the AcceptS of s,x] in UnionSt (s,t)