theorem Th43: :: TURING_1:43

for T1, T2 being TuringStr
for g being Tran-Goal of T1
for p being State of T1
for y being Symbol of T1 st p <> the AcceptS of T1 & g = the Tran of T1 . [p,y] holds
the Tran of (T1 ';' T2) . [[p, the InitS of T2],y] = [[(g `1_3), the InitS of T2],(g `2_3),(g `3_3)]