let IAlph, OAlph be non empty set ; :: thesis: for M1, M2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph holds
( M1,M2 -are_isomorphic iff M1,M2 -are_equivalent )
let M1, M2 be non empty finite reduced connected Mealy-FSM over IAlph,OAlph; :: thesis: ( M1,M2 -are_isomorphic iff M1,M2 -are_equivalent )
thus ( M1,M2 -are_isomorphic implies M1,M2 -are_equivalent ) by Th63; :: thesis: ( M1,M2 -are_equivalent implies M1,M2 -are_isomorphic )
A1: M2, the_reduction_of M2 -are_isomorphic by Th46;
assume M1,M2 -are_equivalent ; :: thesis: M1,M2 -are_isomorphic
then A2: the_reduction_of M1, the_reduction_of M2 -are_isomorphic by Th65;
M1, the_reduction_of M1 -are_isomorphic by Th46;
then M1, the_reduction_of M2 -are_isomorphic by A2, Th42;
hence M1,M2 -are_isomorphic by A1, Th42; :: thesis: verum