let E be non empty set ; :: thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))}
let A be non empty automaton over (Lex E) \/ {(<%> E)}; :: thesis: the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))}
the InitS of (_bool A) = the InitS of semiautomaton(# the carrier of (_bool A), the Tran of (_bool A), the InitS of (_bool A) #)
.= the InitS of (_bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #)) by Def6
.= {((<%> E) -succ_of ( the InitS of semiautomaton(# the carrier of A, the Tran of A, the InitS of A #),semiautomaton(# the carrier of A, the Tran of A, the InitS of A #)))} by Def3 ;
hence the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))} by REWRITE3:105; :: thesis: verum