let X be set ; 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 ; 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 ; 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)}; 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
;
verum