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 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 of (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 of (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 Th36;
hence w -succ_of the InitS of (_bool A),(_bool A) = {(w -succ_of the InitS of A,A)} by Th37; :: thesis: verum