let IAlph, OAlph be non empty set ; :: thesis:
let rtfsm, tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis:
let qr1, qr2 be State of rtfsm; :: thesis:
assume A1: ( rtfsm = the_reduction_of tfsm & qr1 <> qr2 ) ; :: thesis:
then A2: the carrier of rtfsm = final_states_partition tfsm by Def18;
then reconsider q1' = qr1 as Subset of tfsm by TARSKI:def 3;
consider x being Element of tfsm such that
A3: x in q1' by A2, Th11;
reconsider q2' = qr2 as Subset of tfsm by A2, TARSKI:def 3;
consider y being Element of tfsm such that
A4: y in q2' by A2, Th11;
A5: 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
A6: ( x in X & y in X ) by A2, A5, Def14;
X is Subset of tfsm by A2, TARSKI:def 3;
then A7: ( X = q1' or X misses q1' ) by A2, EQREL_1:def 6;
q2' misses q1' by A1, A2, EQREL_1:def 6;
hence contradiction by A3, A4, A6, A7, XBOOLE_0:3; :: thesis:

end;

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

now

assume A21: qr1,w -response = qr2,w -response ; :: thesis:
len w = len (x,w -response ) by Def6;
then A22: k in dom w by A9, FINSEQ_3:27;
then A23: (qr1,w -response ) . k = the OFun of rtfsm . ((qr1,w -admissible ) . k),(w . k) by Def6
.= the OFun of tfsm . ((x,w -admissible ) . k),(w . k) by A1, A12, A14, A15, A17, Def18 ;
A24: (qr2,w -response ) . k = the OFun of rtfsm . ((qr2,w -admissible ) . k),(w . k) by A22, Def6
.= the OFun of tfsm . ((y,w -admissible ) . k),(w . k) by A1, A14, A18, A19, A20, Def18 ;
(x,w -response ) . k = the OFun of tfsm . ((x,w -admissible ) . k),(w . k) by A22, Def6;
hence contradiction by A9, A21, A22, A23, A24, Def6; :: thesis:

end;

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