consider A being non empty finite set , T being Function of [:A,X:],A, I being Element of A;
take S = FSM(# A,T,I #); :: thesis: ( not S is empty & S is finite )
thus not S is empty ; :: thesis: S is finite
thus S is finite ; :: thesis: verum