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