let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for SA being non empty semiautomaton of 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 of F holds the carrier of (_bool SA) = bool the carrier of SA
let SA be non empty semiautomaton of 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