let IAlph, OAlph be non empty set ; :: thesis:
let tfsm, rtfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis:
let qr1, qr2 be State of rtfsm; :: thesis:
assume that
A1: rtfsm = the_reduction_of tfsm and
A2: qr1 <> qr2 ; :: thesis:
A3: the carrier of rtfsm = final_states_partition tfsm by A1, Def18;
then reconsider q19 = qr1 as Subset of tfsm by TARSKI:def 3;
consider x being Element of tfsm such that
A4: x in q19 by A3, FINSEQ_4:87;
reconsider q29 = qr2 as Subset of tfsm by A3, TARSKI:def 3;
consider y being Element of tfsm such that
A5: y in q29 by A3, FINSEQ_4:87;
A6: final_states_partition tfsm is final by Def15;
not x,y -are_equivalent

proof

assume x,y -are_equivalent ; :: thesis:
then consider X being Element of rtfsm such that
A7: ( x in X & y in X ) by A3, A6;
A8: q29 misses q19 by A2, A3, EQREL_1:def 4;
X is Subset of tfsm by A3, TARSKI:def 3;
then ( X = q19 or X misses q19 ) by A3, EQREL_1:def 4;
hence contradiction by A4, A5, A7, A8, XBOOLE_0:3; :: thesis:

end;

then consider w being FinSequence of IAlph such that
A9: (x,w) -response <> (y,w) -response ;
set q1adm = (qr1,w) -admissible ;
set q2adm = (qr2,w) -admissible ;
set xadm = (x,w) -admissible ;
set yadm = (y,w) -admissible ;
set xresp = (x,w) -response ;
set yresp = (y,w) -response ;
len ((x,w) -response) = len w by Def6
.= len ((y,w) -response) by Def6 ;
then consider k being Nat such that
A10: ( 1 <= k & k <= len ((x,w) -response) ) and
A11: ((x,w) -response) . k <> ((y,w) -response) . k by A9, FINSEQ_1:14;
len ((x,w) -response) = len w by Def6;
then A12: k in Seg (len w) by A10, FINSEQ_1:1;
then k in Seg ((len w) + 1) by FINSEQ_2:8;
then A13: ((y,w) -admissible) . k in ((qr2,w) -admissible) . k by A1, A5, Th40;
set q1resp = (qr1,w) -response ;
set q2resp = (qr2,w) -response ;
A14: len ((qr1,w) -admissible) = (len w) + 1 by Def2
.= (len ((x,w) -response)) + 1 by Def6 ;
k in Seg (len ((x,w) -response)) by A10, FINSEQ_1:1;
then A15: k in Seg (len ((qr1,w) -admissible)) by A14, FINSEQ_2:8;
then k in dom ((qr1,w) -admissible) by FINSEQ_1:def 3;
then A16: ((qr1,w) -admissible) . k is Element of rtfsm by FINSEQ_2:11;
len ((qr2,w) -admissible) = (len w) + 1 by Def2
.= len ((qr1,w) -admissible) by Def2 ;
then k in dom ((qr2,w) -admissible) by A15, FINSEQ_1:def 3;
then A17: ((qr2,w) -admissible) . k is Element of rtfsm by FINSEQ_2:11;
k in dom w by A12, FINSEQ_1:def 3;
then A18: w . k is Element of IAlph by FINSEQ_2:11;
A19: len ((qr1,w) -admissible) = (len w) + 1 by Def2
.= len ((x,w) -admissible) by Def2 ;
then k in dom ((x,w) -admissible) by A15, FINSEQ_1:def 3;
then A20: ((x,w) -admissible) . k is Element of tfsm by FINSEQ_2:11;
len ((y,w) -admissible) = (len w) + 1 by Def2
.= len ((x,w) -admissible) by Def2 ;
then k in dom ((y,w) -admissible) by A15, A19, FINSEQ_1:def 3;
then A21: ((y,w) -admissible) . k is Element of tfsm by FINSEQ_2:11;
k in Seg ((len w) + 1) by A12, FINSEQ_2:8;
then A22: ((x,w) -admissible) . k in ((qr1,w) -admissible) . k by A1, A4, Th40;

now :: thesis:

assume A23: (qr1,w) -response = (qr2,w) -response ; :: thesis:
len w = len ((x,w) -response) by Def6;
then A24: k in dom w by A10, FINSEQ_3:25;
then A25: ((x,w) -response) . k = the OFun of tfsm . ((((x,w) -admissible) . k),(w . k)) by Def6;
A26: ((qr2,w) -response) . k = the OFun of rtfsm . ((((qr2,w) -admissible) . k),(w . k)) by A24, Def6
.= the OFun of tfsm . ((((y,w) -admissible) . k),(w . k)) by A1, A18, A17, A13, A21, Def18 ;
((qr1,w) -response) . k = the OFun of rtfsm . ((((qr1,w) -admissible) . k),(w . k)) by A24, Def6
.= the OFun of tfsm . ((((x,w) -admissible) . k),(w . k)) by A1, A16, A18, A22, A20, Def18 ;
hence contradiction by A11, A23, A24, A26, A25, Def6; :: thesis:

end;

hence not qr1,qr2 -are_equivalent ; :: thesis: