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 A = automaton(# the non empty finite set ,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:30, RELAT_1:38, REWRITE3:14;
then semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic ;
hence A is deterministic ; :: thesis: verum