reconsider TS = transition-system(# the carrier of SA,the Tran of SA #) as non empty transition-system of 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:50;
then reconsider bSA = semiautomaton(# the carrier of (_bool TS),tSA,iSA #) as non empty strict deterministic semiautomaton of 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