let k be Element of NAT ; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph holds (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph holds (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: (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 ; :: according to SETFAM_1:def 2 :: thesis: ( not X in (k + 1) -eq_states_partition tfsm or ex b₁ being set st
( b₁ in k -eq_states_partition tfsm & X c= b₁ ) )
assume A1: X in (k + 1) -eq_states_partition tfsm ; :: thesis: ex b₁ being set st
( b₁ in k -eq_states_partition tfsm & X c= b₁ )
then reconsider X' = 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, Th11;
reconsider Y = (proj (k -eq_states_partition tfsm)) . q as Element of k -eq_states_partition tfsm ;
reconsider Y' = Y as Element of Class (k -eq_states_EqR tfsm) ;
take Y ; :: thesis: ( Y in k -eq_states_partition tfsm & X c= Y )
thus Y in k -eq_states_partition tfsm ; :: thesis: X c= Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume A3: x in X ; :: thesis: x in Y
then x in X' ;
then reconsider x' = x as Element of the carrier of tfsm ;
reconsider X' = X' as Element of Class ((k + 1) -eq_states_EqR tfsm) by A1;
consider Q being set such that
A4: ( Q in the carrier of tfsm & X' = Class ((k + 1) -eq_states_EqR tfsm),Q ) by EQREL_1:def 5;
A5: [q,Q] in (k + 1) -eq_states_EqR tfsm by A2, A4, EQREL_1:27;
[x',Q] in (k + 1) -eq_states_EqR tfsm by A3, A4, EQREL_1:27;
then [Q,x'] in (k + 1) -eq_states_EqR tfsm by EQREL_1:12;
then [q,x'] in (k + 1) -eq_states_EqR tfsm by A5, EQREL_1:13;
then k + 1 -equivalent q,x' by Def12;
then k -equivalent q,x' by Th43;
then [q,x'] in k -eq_states_EqR tfsm by Def12;
then A6: [x',q] in k -eq_states_EqR tfsm by EQREL_1:12;
consider Q being set such that
A7: ( Q in the carrier of tfsm & Y' = Class (k -eq_states_EqR tfsm),Q ) by EQREL_1:def 5;
reconsider Q = Q as Element of the carrier of tfsm by A7;
q in Y by BORSUK_1:def 1;
then Class (k -eq_states_EqR tfsm),Q = Class (k -eq_states_EqR tfsm),q by A7, EQREL_1:31;
hence x in Y by A6, A7, EQREL_1:27; :: thesis: verum