let X be set ; :: thesis: for E being non empty set
for w being Element of E ^omega
for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))}
let E be non empty set ; :: thesis: for w being Element of E ^omega
for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))}
let w be Element of E ^omega ; :: thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))}
let A be non empty automaton over (Lex E) \/ {(<%> E)}; :: thesis: w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))}
set SA = semiautomaton(# the carrier of A, the Tran of A, the InitS of A #);
set Es = (<%> E) -succ_of (X,A);
semiautomaton(# the carrier of (_bool A), the Tran of (_bool A), the InitS of (_bool A) #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) by Def6;
hence w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = w -succ_of ({((<%> E) -succ_of (X,A))},(_bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #))) by REWRITE3:105
.= w -succ_of ({((<%> E) -succ_of (X,semiautomaton(# the carrier of A, the Tran of A, the InitS of A #)))},(_bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #))) by REWRITE3:105
.= {(w -succ_of (X,semiautomaton(# the carrier of A, the Tran of A, the InitS of A #)))} by Th32
.= {(w -succ_of (X,A))} by REWRITE3:105 ;
:: thesis: verum