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