let w be Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0 ,1}:]; :: thesis: ( ex p being State of s ex y being Symbol of s st
( x = [[p,the InitS of t],y] & p <> the AcceptS of s ) & ex q being State of t ex y being Symbol of t st x = [[the AcceptS of s,q],y] implies ( w = FirstTuringTran s,t,(the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)]) iff w = SecondTuringTran s,t,(the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)]) ) )
thus ( ex p being State of s ex y being Symbol of s st
( x = [[p,the InitS of t],y] & p <> the AcceptS of s ) & ex q being State of t ex y being Symbol of t st x = [[the AcceptS of s,q],y] implies ( w = FirstTuringTran s,t,(the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)]) iff w = SecondTuringTran s,t,(the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)]) ) ) :: thesis: verum

proof

given p being State of s, y being Symbol of s such that A1: x = [[p,the InitS of t],y] and
A2: p <> the AcceptS of s ; :: thesis: ( for q being State of t
for y being Symbol of t holds not x = [[the AcceptS of s,q],y] or ( w = FirstTuringTran s,t,(the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)]) iff w = SecondTuringTran s,t,(the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)]) ) )
given q being State of t, z being Symbol of t such that A3: x = [[the AcceptS of s,q],z] ; :: thesis: ( w = FirstTuringTran s,t,(the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)]) iff w = SecondTuringTran s,t,(the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)]) )
[p,the InitS of t] = [the AcceptS of s,q] by A1, A3, ZFMISC_1:33;
hence ( w = FirstTuringTran s,t,(the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)]) iff w = SecondTuringTran s,t,(the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)]) ) by A2, ZFMISC_1:33; :: thesis: verum

end;