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