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