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