let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds
( tfsm is reduced iff ex M being non empty finite Mealy-FSM over IAlph,OAlph st tfsm, the_reduction_of M -are_isomorphic )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: ( tfsm is reduced iff ex M being non empty finite Mealy-FSM over IAlph,OAlph st tfsm, the_reduction_of M -are_isomorphic )
set M = tfsm;

hereby :: thesis: ( ex M being non empty finite Mealy-FSM over IAlph,OAlph st tfsm, the_reduction_of M -are_isomorphic implies tfsm is reduced )

assume tfsm is reduced ; :: thesis: ex M being non empty finite Mealy-FSM over IAlph,OAlph st tfsm, the_reduction_of M -are_isomorphic
then tfsm, the_reduction_of tfsm -are_isomorphic by Th46;
hence ex M being non empty finite Mealy-FSM over IAlph,OAlph st tfsm, the_reduction_of M -are_isomorphic ; :: thesis: verum

end;

given MM being non empty finite Mealy-FSM over IAlph,OAlph such that A1: tfsm, the_reduction_of MM -are_isomorphic ; :: thesis: tfsm is reduced
set rMM = the_reduction_of MM;
consider Tf being Function of the carrier of tfsm, the carrier of (the_reduction_of MM) such that
A2: Tf is bijective and
Tf . the InitS of tfsm = the InitS of (the_reduction_of MM) and
A3: for q being State of tfsm
for s being Element of IAlph holds
( Tf . ( the Tran of tfsm . (q,s)) = the Tran of (the_reduction_of MM) . ((Tf . q),s) & the OFun of tfsm . (q,s) = the OFun of (the_reduction_of MM) . ((Tf . q),s) ) by A1;
let qa, qb be State of tfsm; :: according to FSM_1:def 20 :: thesis: ( qa <> qb implies not qa,qb -are_equivalent )
assume qa <> qb ; :: thesis: not qa,qb -are_equivalent
then Tf . qa <> Tf . qb by A2, FUNCT_2:19;
then not Tf . qa,Tf . qb -are_equivalent by Th45;
hence not qa,qb -are_equivalent by A3, Th44; :: thesis: verum