consider X being non empty finite set ;
reconsider T = {} as Relation of [:X,F:],X by RELSET_1:25;
consider x being Element of X;
reconsider I = {x} as Subset of X ;
take SA = semiautomaton(# X,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:60, 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:50; :: thesis: verum