theorem Th15: :: FSM_3:15

for E being non empty set
for w being Element of E ^omega
for F being Subset of (E ^omega)
for SA being non empty semiautomaton over F
for Q being Subset of SA holds
( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )