:: deftheorem defines left-Lang FSM_3:def 4 :
for E being non empty set
for F being Subset of (E ^omega)
for SA being non empty semiautomaton over F
for Q being Subset of SA holds left-Lang Q = { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ;