let k be Nat; for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph holds (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
let IAlph, OAlph be non empty set ; for tfsm being non empty Mealy-FSM over IAlph,OAlph holds (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
let tfsm be non empty Mealy-FSM over IAlph,OAlph; (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
set K = k -eq_states_partition tfsm;
set K1 = (k + 1) -eq_states_partition tfsm;
set S = the carrier of tfsm;
let X be set ; SETFAM_1:def 2 ( not X in (k + 1) -eq_states_partition tfsm or ex b1 being set st
( b1 in k -eq_states_partition tfsm & X c= b1 ) )
assume A1:
X in (k + 1) -eq_states_partition tfsm
; ex b1 being set st
( b1 in k -eq_states_partition tfsm & X c= b1 )
then reconsider X9 = X as Subset of the carrier of tfsm ;
consider q being Element of the carrier of tfsm such that
A2:
q in X
by A1, FINSEQ_4:87;
reconsider Y = (proj (k -eq_states_partition tfsm)) . q as Element of k -eq_states_partition tfsm ;
take
Y
; ( Y in k -eq_states_partition tfsm & X c= Y )
thus
Y in k -eq_states_partition tfsm
; X c= Y
let x be object ; TARSKI:def 3 ( not x in X or x in Y )
assume A3:
x in X
; x in Y
then
x in X9
;
then reconsider x9 = x as Element of the carrier of tfsm ;
reconsider X9 = X9 as Element of Class ((k + 1) -eq_states_EqR tfsm) by A1;
consider Q being object such that
Q in the carrier of tfsm
and
A4:
X9 = Class (((k + 1) -eq_states_EqR tfsm),Q)
by EQREL_1:def 3;
[x9,Q] in (k + 1) -eq_states_EqR tfsm
by A3, A4, EQREL_1:19;
then A5:
[Q,x9] in (k + 1) -eq_states_EqR tfsm
by EQREL_1:6;
[q,Q] in (k + 1) -eq_states_EqR tfsm
by A2, A4, EQREL_1:19;
then
[q,x9] in (k + 1) -eq_states_EqR tfsm
by A5, EQREL_1:7;
then
k + 1 -equivalent q,x9
by Def12;
then
k -equivalent q,x9
by Th26;
then
[q,x9] in k -eq_states_EqR tfsm
by Def12;
then A6:
[x9,q] in k -eq_states_EqR tfsm
by EQREL_1:6;
reconsider Y9 = Y as Element of Class (k -eq_states_EqR tfsm) ;
consider Q being object such that
A7:
Q in the carrier of tfsm
and
A8:
Y9 = Class ((k -eq_states_EqR tfsm),Q)
by EQREL_1:def 3;
reconsider Q = Q as Element of the carrier of tfsm by A7;
q in Y
by EQREL_1:def 9;
then
Class ((k -eq_states_EqR tfsm),Q) = Class ((k -eq_states_EqR tfsm),q)
by A8, EQREL_1:23;
hence
x in Y
by A6, A8, EQREL_1:19; verum