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 ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))}
let w be Element of E ^omega ; :: thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))}
let A be non empty automaton over (Lex E) \/ {(<%> E)}; :: thesis: w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))}
set Es = (<%> E) -succ_of ( the InitS of A,A);
the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))} by Th35;
hence w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} by Th36; :: thesis: verum