:: deftheorem Def5 defines deterministic FSM_3:def 5 :
for E being non empty set
for F being Subset of (E ^omega)
for A being automaton over F holds
( A is deterministic iff semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic );