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 ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,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 ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) )
let F be Subset of (E ^omega); :: thesis: for A being non empty automaton over F holds
( w in Lang A iff ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) )
let A be non empty automaton over F; :: thesis: ( w in Lang A iff ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) )
thus ( w in Lang A implies ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ) :: thesis: ( ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) implies w in Lang A )

proof

assume w in Lang A ; :: thesis: ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A )
then ex u being Element of E ^omega st
( w = u & ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) ) ;
hence ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ; :: thesis: verum

end;

thus ( ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) implies w in Lang A ) ; :: thesis: verum