:: deftheorem Def6 defines _bool FSM_3:def 6 :
for E being non empty set
for F being Subset of (E ^omega)
for A being non empty automaton over F
for b₄ being strict automaton over Lex E holds
( b₄ = _bool A iff ( semiautomaton(# the carrier of b₄, the Tran of b₄, the InitS of b₄ #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b₄ = { Q where Q is Element of b₄ : Q meets the FinalS of A } ) );