theorem Th19: :: FSM_3:19

for E being non empty set
for w being Element of E ^omega
for F being Subset of (E ^omega)
for A being non empty automaton over F holds
( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A )