reconsider l = - 1 as Element of {(- 1),0 ,1} by ENUMSET1:def 1;
[(x `1 ),(x `2 ),l] in [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0 ,1}:] ;
hence ( ( 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 ) implies FirstTuringTran s,t,(the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)]) is Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0 ,1}:] ) & ( ex q being State of t ex y being Symbol of t st x = [[the AcceptS of s,q],y] implies SecondTuringTran s,t,(the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)]) is Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0 ,1}:] ) & ( ( for p being State of s
for y being Symbol of s holds
( not x = [[p,the InitS of t],y] or not p <> the AcceptS of s ) ) & ( for q being State of t
for y being Symbol of t holds not x = [[the AcceptS of s,q],y] ) implies [(x `1 ),(x `2 ),(- 1)] is Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0 ,1}:] ) ) ; :: thesis: verum