for T1, T2 being TuringStr
for s1 being All-State of T1
for h being Element of NAT
for t being Tape of T1
for s2 being All-State of T2
for s3 being All-State of (T1 ';' T2) st s1 is Accept-Halt & s1 = [ the InitS of T1,h,t] & s2 is Accept-Halt & s2 = [ the InitS of T2,((Result s1) `2_3),((Result s1) `3_3)] & s3 = [ the InitS of (T1 ';' T2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_3 )