consider X being non empty finite set , T being Function of [:X,IAlph:],X, O being Function of X,OAlph, I being Element of X;
take Moore-FSM(# X,T,O,I #) ; :: thesis: ( Moore-FSM(# X,T,O,I #) is finite & not Moore-FSM(# X,T,O,I #) is empty )
thus ( Moore-FSM(# X,T,O,I #) is finite & not Moore-FSM(# X,T,O,I #) is empty ) ; :: thesis: verum