let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for SA being non empty semiautomaton over F holds the carrier of (_bool SA) = bool the carrier of SA
let F be Subset of (E ^omega); :: thesis: for SA being non empty semiautomaton over F holds the carrier of (_bool SA) = bool the carrier of SA
let SA be non empty semiautomaton over F; :: thesis: the carrier of (_bool SA) = bool the carrier of SA
transition-system(# the carrier of (_bool SA), the Tran of (_bool SA) #) = _bool transition-system(# the carrier of SA, the Tran of SA #) by Def3;
hence the carrier of (_bool SA) = bool the carrier of SA by Def1; :: thesis: verum