let X be set ; :: thesis: for E being non empty set
for w being Element of E ^omega
for A being non empty automaton of (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 of (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 of (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 of (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 Th33
.= {(w -succ_of X,A)} by REWRITE3:105 ;
:: thesis: verum