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 A = automaton(# X,T,I,I #); :: thesis: ( A is strict & not A is empty & A is finite & A is deterministic )
thus A is strict ; :: thesis: ( not A is empty & A is finite & A is deterministic )
thus not A is empty ; :: thesis: ( A is finite & A is deterministic )
thus the carrier of A is finite ; :: according to STRUCT_0:def 11 :: thesis: A is deterministic
( transition-system(# the carrier of A,the Tran of A #) is deterministic & card the InitS of A = 1 ) by CARD_1:50, RELAT_1:60, REWRITE3:14;
then semiautomaton(# the carrier of A,the Tran of A,the InitS of A #) is deterministic by Def2;
hence A is deterministic by Def5; :: thesis: verum