theorem Th42: :: TURING_1:42

for s, t being TuringStr
for x being Element of UnionSt (s,t) ex x1 being State of s ex x2 being State of t st x = [x1,x2]