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

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