let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for A being non empty automaton of F holds the carrier of (_bool A) = bool the carrier of A
let F be Subset of (E ^omega ); :: thesis: for A being non empty automaton of F holds the carrier of (_bool A) = bool the carrier of A
let A be non empty automaton of F; :: thesis: the carrier of (_bool A) = bool the carrier of 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 defBoolA;
hence the carrier of (_bool A) = bool the carrier of A by ThSA10; :: thesis: verum