let X be set ; :: thesis: for E being non empty set
for w being Element of E ^omega
for SA being non empty semiautomaton over (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 over (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 over (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 over (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
.= {(({} ^ w) -succ_of (X,transition-system(# the carrier of SA, the Tran of SA #)))} by Th31
.= {(w -succ_of (X,transition-system(# the carrier of SA, the Tran of SA #)))}
.= {(w -succ_of (X,SA))} by REWRITE3:105 ;
:: thesis: verum