let E be 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 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 ; 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); 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; ( 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 ) )
( 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 )
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 )
; verum