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