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}:] ) )
; verum