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

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