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 holds

( w in Lang A iff w -succ_of ( the InitS of A,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 holds

( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A )

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

let A be non empty automaton over F; :: thesis: ( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A )

thus ( w in Lang A implies w -succ_of ( the InitS of A,A) meets the FinalS of A ) :: thesis: ( w -succ_of ( the InitS of A,A) meets the FinalS of A implies w in Lang A )

then consider x being object such that

A4: x in w -succ_of ( the InitS of A,A) and

A5: x in the FinalS of A by XBOOLE_0:3;

reconsider x = x as Element of A by A4;

ex p being Element of A st

( p in the InitS of A & p,w ==>* x,A ) by A4, REWRITE3:103;

hence w in Lang A by A5; :: thesis: verum

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 )

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

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

let A be non empty automaton over F; :: thesis: ( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A )

thus ( w in Lang A implies w -succ_of ( the InitS of A,A) meets the FinalS of A ) :: thesis: ( w -succ_of ( the InitS of A,A) meets the FinalS of A implies w in Lang A )

proof

assume
w -succ_of ( the InitS of A,A) meets the FinalS of A
; :: thesis: w in Lang A
assume
w in Lang A
; :: thesis: w -succ_of ( the InitS of A,A) meets the FinalS of A

then consider p, q being Element of A such that

A1: p in the InitS of A and

A2: q in the FinalS of A and

A3: p,w ==>* q,A by Th18;

q in w -succ_of ( the InitS of A,A) by A1, A3, REWRITE3:103;

hence w -succ_of ( the InitS of A,A) meets the FinalS of A by A2, XBOOLE_0:3; :: thesis: verum

end;then consider p, q being Element of A such that

A1: p in the InitS of A and

A2: q in the FinalS of A and

A3: p,w ==>* q,A by Th18;

q in w -succ_of ( the InitS of A,A) by A1, A3, REWRITE3:103;

hence w -succ_of ( the InitS of A,A) meets the FinalS of A by A2, XBOOLE_0:3; :: thesis: verum

then consider x being object such that

A4: x in w -succ_of ( the InitS of A,A) and

A5: x in the FinalS of A by XBOOLE_0:3;

reconsider x = x as Element of A by A4;

ex p being Element of A st

( p in the InitS of A & p,w ==>* x,A ) by A4, REWRITE3:103;

hence w in Lang A by A5; :: thesis: verum