theorem Th40: :: TURING_1:40

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