set cm = the non empty finite connected Mealy-FSM over IAlph,OAlph;
take the_reduction_of the non empty finite connected Mealy-FSM over IAlph,OAlph ; :: thesis: ( the_reduction_of the non empty finite connected Mealy-FSM over IAlph,OAlph is connected & the_reduction_of the non empty finite connected Mealy-FSM over IAlph,OAlph is reduced & the_reduction_of the non empty finite connected Mealy-FSM over IAlph,OAlph is finite )
thus ( the_reduction_of the non empty finite connected Mealy-FSM over IAlph,OAlph is connected & the_reduction_of the non empty finite connected Mealy-FSM over IAlph,OAlph is reduced & the_reduction_of the non empty finite connected Mealy-FSM over IAlph,OAlph is finite ) ; :: thesis: verum