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