set X = the non empty finite set ;
reconsider T = {} as Relation of [: the non empty finite set ,F:], the non empty finite set by RELSET_1:12;
set x = the Element of the non empty finite set ;
reconsider I = { the Element of the non empty finite set } as Subset of the non empty finite set ;
take SA = semiautomaton(# the non empty finite set ,T,I #); :: thesis: ( SA is strict & not SA is empty & SA is finite & SA is deterministic )
thus SA is strict ; :: thesis: ( not SA is empty & SA is finite & SA is deterministic )
thus not SA is empty ; :: thesis: ( SA is finite & SA is deterministic )
thus the carrier of SA is finite ; :: according to STRUCT_0:def 11 :: thesis: SA is deterministic
thus transition-system(# the carrier of SA, the Tran of SA #) is deterministic by RELAT_1:38, REWRITE3:14; :: according to FSM_3:def 2 :: thesis: card the InitS of SA = 1
thus card the InitS of SA = 1 by CARD_1:30; :: thesis: verum