:: deftheorem Def2 defines deterministic FSM_3:def 2 :
for E being non empty set
for F being Subset of (E ^omega)
for SA being semiautomaton over F holds
( SA is deterministic iff ( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 ) );