reconsider TS = transition-system(# the carrier of SA, the Tran of SA #) as non empty transition-system over F ;
set cSA = the carrier of (_bool TS);
reconsider iSA = {((<%> E) -succ_of ( the InitS of SA,SA))} as Subset of the carrier of (_bool TS) by Def1;
reconsider tSA = the Tran of (_bool TS) as Relation of [: the carrier of (_bool TS),(Lex E):], the carrier of (_bool TS) ;
set bSA = semiautomaton(# the carrier of (_bool TS),tSA,iSA #);
card iSA = 1 by CARD_1:30;
then reconsider bSA = semiautomaton(# the carrier of (_bool TS),tSA,iSA #) as non empty strict deterministic semiautomaton over Lex E by Def2;
take bSA ; :: thesis: ( transition-system(# the carrier of bSA, the Tran of bSA #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of bSA = {((<%> E) -succ_of ( the InitS of SA,SA))} )
thus ( transition-system(# the carrier of bSA, the Tran of bSA #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of bSA = {((<%> E) -succ_of ( the InitS of SA,SA))} ) ; :: thesis: verum