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 . [(),])) iff w = SecondTuringTran (s,t,( the Tran of t . )) ) )

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 . [(),])) iff w = SecondTuringTran (s,t,( the Tran of t . )) ) ) :: 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 . [(),])) iff w = SecondTuringTran (s,t,( the Tran of t . )) ) )

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 . [(),])) iff w = SecondTuringTran (s,t,( the Tran of t . )) )
[p, the InitS of t] = [ the AcceptS of s,q] by ;
hence ( w = FirstTuringTran (s,t,( the Tran of s . [(),])) iff w = SecondTuringTran (s,t,( the Tran of t . )) ) by ; :: thesis: verum
end;