let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for qa, qb being State of tfsm st qa,qb -are_equivalent holds
for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
let qa, qb be State of tfsm; :: thesis: ( qa,qb -are_equivalent implies for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent ) )
assume A1: qa,qb -are_equivalent ; :: thesis: for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
let w be FinSequence of IAlph; :: thesis: for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
defpred S₁[ Nat] means ( $1 in Seg (len w) implies ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . $1 & qbi = ((qb,w) -admissible) . $1 & qai,qbi -are_equivalent ) );
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: ( i in Seg (len w) implies ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent ) ) ; :: thesis: S₁[i + 1]
A4: ( i = 0 or ( 0 < i & 0 + 1 = 1 ) ) ;
assume i + 1 in Seg (len w) ; :: thesis: ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )
then i + 1 <= len w by FINSEQ_1:1;
then A5: ( 0 = i or ( 1 <= i & i <= len w ) ) by A4, NAT_1:13;

per cases ( i = 0 or i in Seg (len w) ) by A5, FINSEQ_1:1;

suppose A6: i = 0 ; :: thesis: ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )

reconsider qai = ((qa,w) -admissible) . 1, qbi = ((qb,w) -admissible) . 1 as Element of tfsm by Def2;
take qai ; :: thesis: ex qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )
take qbi ; :: thesis: ( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )
thus qai = ((qa,w) -admissible) . (i + 1) by A6; :: thesis: ( qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )
thus qbi = ((qb,w) -admissible) . (i + 1) by A6; :: thesis: qai,qbi -are_equivalent
qai = qa by Def2;
hence qai,qbi -are_equivalent by A1, Def2; :: thesis: verum

end;

suppose A7: i in Seg (len w) ; :: thesis: ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )

then A8: ( 1 <= i & i <= len w ) by FINSEQ_1:1;
then consider wi being Element of IAlph, qai9, qai19 being Element of tfsm such that
A9: ( wi = w . i & qai9 = ((qa,w) -admissible) . i ) and
A10: qai19 = ((qa,w) -admissible) . (i + 1) and
A11: wi -succ_of qai9 = qai19 by Def2;
take qai19 ; :: thesis: ex qbi being Element of tfsm st
( qai19 = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai19,qbi -are_equivalent )
consider wi9 being Element of IAlph, qbi9, qbi19 being Element of tfsm such that
A12: ( wi9 = w . i & qbi9 = ((qb,w) -admissible) . i ) and
A13: qbi19 = ((qb,w) -admissible) . (i + 1) and
A14: wi9 -succ_of qbi9 = qbi19 by A8, Def2;
take qbi19 ; :: thesis: ( qai19 = ((qa,w) -admissible) . (i + 1) & qbi19 = ((qb,w) -admissible) . (i + 1) & qai19,qbi19 -are_equivalent )
thus qai19 = ((qa,w) -admissible) . (i + 1) by A10; :: thesis: ( qbi19 = ((qb,w) -admissible) . (i + 1) & qai19,qbi19 -are_equivalent )
thus qbi19 = ((qb,w) -admissible) . (i + 1) by A13; :: thesis: qai19,qbi19 -are_equivalent
thus qai19,qbi19 -are_equivalent by A3, A7, A9, A11, A12, A14, Th19; :: thesis: verum

end;

end;

end;

A15: Seg (len w) = dom w by FINSEQ_1:def 3;
A16: S₁[ 0 ] by FINSEQ_1:1;
for i being Nat holds S₁[i] from NAT_1:sch 2(A16, A2);
hence for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent ) by A15; :: thesis: verum