let E be non empty set ; :: thesis: for A being non empty automaton of (Lex E) \/ {(<%> E)} holds the InitS of (_bool A) = {((<%> E) -succ_of the InitS of A,A)}
let A be non empty automaton of (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