:: deftheorem defines Lang FSM_3:def 8 :
for E being non empty set
for F being Subset of (E ^omega)
for A being non empty automaton over F holds Lang A = { u where u is Element of E ^omega : ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } ;