let E be non empty set ; :: thesis: for A being non empty automaton of (Lex E) \/ {(<%> E)} holds Lang A = Lang (_bool A)
let A be non empty automaton of (Lex E) \/ {(<%> E)}; :: thesis: Lang A = Lang (_bool A)
set DA = _bool A;
A:
for w being Element of E ^omega st w in Lang A holds
w in Lang (_bool A)
proof
let w be
Element of
E ^omega ;
:: thesis: ( w in Lang A implies w in Lang (_bool A) )
assume
w in Lang A
;
:: thesis: w in Lang (_bool A)
then
w -succ_of the
InitS of
A,
A meets the
FinalS of
A
by ThLang10;
then consider x being
set such that B:
(
x in w -succ_of the
InitS of
A,
A &
x in the
FinalS of
A )
by XBOOLE_0:3;
C:
w -succ_of the
InitS of
A,
A in the
FinalS of
(_bool A)
by B, ThA20;
w -succ_of the
InitS of
(_bool A),
(_bool A) = {(w -succ_of the InitS of A,A)}
by ThA40;
then
w -succ_of the
InitS of
A,
A in w -succ_of the
InitS of
(_bool A),
(_bool A)
by TARSKI:def 1;
then
w -succ_of the
InitS of
(_bool A),
(_bool A) meets the
FinalS of
(_bool A)
by C, XBOOLE_0:3;
hence
w in Lang (_bool A)
by ThLang10;
:: thesis: verum
end;
for w being Element of E ^omega st w in Lang (_bool A) holds
w in Lang A
hence
Lang A = Lang (_bool A)
by A, SUBSET_1:8; :: thesis: verum