consider cm being non empty finite connected Mealy-FSM of IAlph,OAlph;
take the_reduction_of cm ; :: thesis: ( the_reduction_of cm is connected & the_reduction_of cm is reduced & the_reduction_of cm is finite )
thus ( the_reduction_of cm is connected & the_reduction_of cm is reduced & the_reduction_of cm is finite ) ; :: thesis: verum