let IAlph, OAlph be non empty set ; :: thesis: for Rtfsm being non empty finite reduced Mealy-FSM over IAlph,OAlph holds Rtfsm, the_reduction_of Rtfsm -are_isomorphic
let Rtfsm be non empty finite reduced Mealy-FSM over IAlph,OAlph; :: thesis: Rtfsm, the_reduction_of Rtfsm -are_isomorphic
set m = Rtfsm;
set rm = the_reduction_of Rtfsm;
set fpm = final_states_partition Rtfsm;
deffunc H₁( Element of Rtfsm) -> Element of final_states_partition Rtfsm = (proj (final_states_partition Rtfsm)) . $1;
consider Tf being Function of the carrier of Rtfsm,(final_states_partition Rtfsm) such that
A1: for q being Element of Rtfsm holds Tf . q = H₁(q) from FUNCT_2:sch 4();

A2: now :: thesis: Tf is one-to-one

assume not Tf is one-to-one ; :: thesis: contradiction
then consider q1, q2 being object such that
A3: ( q1 in the carrier of Rtfsm & q2 in the carrier of Rtfsm ) and
A4: Tf . q1 = Tf . q2 and
A5: q1 <> q2 by FUNCT_2:19;
reconsider q1 = q1, q2 = q2 as State of Rtfsm by A3;
Tf . q1 = (proj (final_states_partition Rtfsm)) . q1 by A1;
then A6: q1 in Tf . q1 by EQREL_1:def 9;
A7: final_states_partition Rtfsm is final by Def15;
Tf . q2 = (proj (final_states_partition Rtfsm)) . q2 by A1;
then A8: q2 in Tf . q2 by EQREL_1:def 9;
not q1,q2 -are_equivalent by A5, Def20;
hence contradiction by A4, A7, A6, A8; :: thesis: verum

end;

set Im1 = the InitS of Rtfsm;
A9: final_states_partition Rtfsm c= rng Tf

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in final_states_partition Rtfsm or x in rng Tf )
assume A10: x in final_states_partition Rtfsm ; :: thesis: x in rng Tf
then reconsider pq = x as Subset of Rtfsm ;
consider q being Element of Rtfsm such that
A11: q in pq by A10, FINSEQ_4:87;
pq = (proj (final_states_partition Rtfsm)) . q by A10, A11, EQREL_1:65;
then Tf . q = pq by A1;
hence x in rng Tf by FUNCT_2:4; :: thesis: verum

end;

rng Tf c= final_states_partition Rtfsm by RELAT_1:def 19;
then rng Tf = final_states_partition Rtfsm by A9;
then A12: Tf is onto by FUNCT_2:def 3;
A13: the carrier of (the_reduction_of Rtfsm) = final_states_partition Rtfsm by Def18;

A14: now :: thesis: for q being State of Rtfsm
for s being Element of IAlph holds
( Tf . ( the Tran of Rtfsm . (q,s)) = the Tran of (the_reduction_of Rtfsm) . ((Tf . q),s) & the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s) )

let q be State of Rtfsm; :: thesis: for s being Element of IAlph holds
( Tf . ( the Tran of Rtfsm . (q,s)) = the Tran of (the_reduction_of Rtfsm) . ((Tf . q),s) & the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s) )
let s be Element of IAlph; :: thesis: ( Tf . ( the Tran of Rtfsm . (q,s)) = the Tran of (the_reduction_of Rtfsm) . ((Tf . q),s) & the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s) )
reconsider Tfq = Tf . q as State of (the_reduction_of Rtfsm) by Def18;
A15: the Tran of (the_reduction_of Rtfsm) . [Tfq,s] is State of (the_reduction_of Rtfsm) ;
Tf . q = (proj (final_states_partition Rtfsm)) . q by A1;
then A16: q in Tf . q by EQREL_1:def 9;
then the Tran of Rtfsm . (q,s) in the Tran of (the_reduction_of Rtfsm) . ((Tf . q),s) by A13, Def18;
then the Tran of (the_reduction_of Rtfsm) . [(Tf . q),s] = (proj (final_states_partition Rtfsm)) . ( the Tran of Rtfsm . [q,s]) by A13, A15, EQREL_1:65;
hence Tf . ( the Tran of Rtfsm . (q,s)) = the Tran of (the_reduction_of Rtfsm) . ((Tf . q),s) by A1; :: thesis: the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s)
thus the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s) by A13, A16, Def18; :: thesis: verum

end;

the InitS of Rtfsm in the InitS of (the_reduction_of Rtfsm) by Def18;
then the InitS of (the_reduction_of Rtfsm) = (proj (final_states_partition Rtfsm)) . the InitS of Rtfsm by A13, EQREL_1:65;
then Tf . the InitS of Rtfsm = the InitS of (the_reduction_of Rtfsm) by A1;
hence Rtfsm, the_reduction_of Rtfsm -are_isomorphic by A13, A2, A12, A14; :: thesis: verum