let E be non empty set ; :: thesis: for F being Subset of (E ^omega)

for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A

let F be Subset of (E ^omega); :: thesis: for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A

let A be non empty automaton over F; :: thesis: Lang A = left-Lang the FinalS of A

A1: for w being Element of E ^omega st w in Lang A holds

w in left-Lang the FinalS of A

w in Lang A

for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A

let F be Subset of (E ^omega); :: thesis: for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A

let A be non empty automaton over F; :: thesis: Lang A = left-Lang the FinalS of A

A1: for w being Element of E ^omega st w in Lang A holds

w in left-Lang the FinalS of A

proof

for w being Element of E ^omega st w in left-Lang the FinalS of A holds
let w be Element of E ^omega ; :: thesis: ( w in Lang A implies w in left-Lang the FinalS of A )

assume w in Lang A ; :: thesis: w in left-Lang the FinalS of A

then w -succ_of ( the InitS of A,A) meets the FinalS of A by Th19;

hence w in left-Lang the FinalS of A ; :: thesis: verum

end;assume w in Lang A ; :: thesis: w in left-Lang the FinalS of A

then w -succ_of ( the InitS of A,A) meets the FinalS of A by Th19;

hence w in left-Lang the FinalS of A ; :: thesis: verum

w in Lang A

proof

hence
Lang A = left-Lang the FinalS of A
by A1, SUBSET_1:3; :: thesis: verum
let w be Element of E ^omega ; :: thesis: ( w in left-Lang the FinalS of A implies w in Lang A )

assume w in left-Lang the FinalS of A ; :: thesis: w in Lang A

then the FinalS of A meets w -succ_of ( the InitS of A,A) by Th15;

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

end;assume w in left-Lang the FinalS of A ; :: thesis: w in Lang A

then the FinalS of A meets w -succ_of ( the InitS of A,A) by Th15;

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