let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM of IAlph,OAlph holds the_reduction_of tfsm is reduced
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis: the_reduction_of tfsm is reduced
let qa, qb be State of (the_reduction_of tfsm); :: according to FSM_1:def 20 :: thesis: ( qa <> qb implies not qa,qb -are_equivalent )
thus ( qa <> qb implies not qa,qb -are_equivalent ) by Th62; :: thesis: verum