let E be non empty set ; :: thesis: for w being Element of E ^omega
for F being Subset of ()
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 )

let w be Element of E ^omega ; :: thesis: for F being Subset of ()
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 )

let F be Subset of (); :: thesis: 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 )

let A be non empty automaton over F; :: thesis: for Q being Subset of A holds
( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

let Q be Subset of A; :: thesis: ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )
thus ( w in right-Lang Q implies w -succ_of (Q,A) meets the FinalS of A ) :: thesis: ( w -succ_of (Q,A) meets the FinalS of A implies w in right-Lang Q )
proof
assume w in right-Lang Q ; :: thesis: w -succ_of (Q,A) meets the FinalS of A
then ex w9 being Element of E ^omega st
( w = w9 & w9 -succ_of (Q,A) meets the FinalS of A ) ;
hence w -succ_of (Q,A) meets the FinalS of A ; :: thesis: verum
end;
thus ( w -succ_of (Q,A) meets the FinalS of A implies w in right-Lang Q ) ; :: thesis: verum