let IAlph, OAlph be non empty set ; :: thesis: for M1, M2 being non empty finite reduced connected Mealy-FSM of IAlph,OAlph holds
( M1,M2 -are_isomorphic iff M1,M2 -are_equivalent )
let M1, M2 be non empty finite reduced connected Mealy-FSM of IAlph,OAlph; :: thesis: ( M1,M2 -are_isomorphic iff M1,M2 -are_equivalent )
thus ( M1,M2 -are_isomorphic implies M1,M2 -are_equivalent ) by Th82; :: thesis: ( M1,M2 -are_equivalent implies M1,M2 -are_isomorphic )
A1: M2, the_reduction_of M2 -are_isomorphic by Th64;
assume M1,M2 -are_equivalent ; :: thesis: M1,M2 -are_isomorphic
then A2: the_reduction_of M1, the_reduction_of M2 -are_isomorphic by Th84;
M1, the_reduction_of M1 -are_isomorphic by Th64;
then M1, the_reduction_of M2 -are_isomorphic by A2, Th59;
hence M1,M2 -are_isomorphic by A1, Th59; :: thesis: verum