theorem Th17: :: FSM_3:17

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
for Q being Subset of A holds
( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )