:: deftheorem Def3 defines _bool FSM_3:def 3 :
for E being non empty set
for F being Subset of (E ^omega)
for SA being non empty semiautomaton over F
for b₄ being strict semiautomaton over Lex E holds
( b₄ = _bool SA iff ( transition-system(# the carrier of b₄, the Tran of b₄ #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b₄ = {((<%> E) -succ_of ( the InitS of SA,SA))} ) );