let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for A being non empty automaton of F holds Lang A = left-Lang the FinalS of A
let F be Subset of (E ^omega ); :: thesis: for A being non empty automaton of F holds Lang A = left-Lang the FinalS of A
let A be non empty automaton of 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

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 Th20;
hence w in left-Lang the FinalS of A ; :: thesis: verum

end;

for w being Element of E ^omega st w in left-Lang the FinalS of A holds
w in Lang A

proof

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 Th16;
hence w in Lang A by Th20; :: thesis: verum

end;

hence Lang A = left-Lang the FinalS of A by A1, SUBSET_1:8; :: thesis: verum