let k be Nat; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds
( k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm or card (k -eq_states_partition tfsm) < card ((k + 1) -eq_states_partition tfsm) )
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds
( k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm or card (k -eq_states_partition tfsm) < card ((k + 1) -eq_states_partition tfsm) )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: ( k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm or card (k -eq_states_partition tfsm) < card ((k + 1) -eq_states_partition tfsm) )
set kp = k -eq_states_partition tfsm;
set k1p = (k + 1) -eq_states_partition tfsm;
card (k -eq_states_partition tfsm) <= card ((k + 1) -eq_states_partition tfsm) by Th28, FINSEQ_4:89;
then A1: ( card (k -eq_states_partition tfsm) = card ((k + 1) -eq_states_partition tfsm) or card (k -eq_states_partition tfsm) < card ((k + 1) -eq_states_partition tfsm) ) by XXREAL_0:1;
assume k -eq_states_partition tfsm <> (k + 1) -eq_states_partition tfsm ; :: thesis: card (k -eq_states_partition tfsm) < card ((k + 1) -eq_states_partition tfsm)
hence card (k -eq_states_partition tfsm) < card ((k + 1) -eq_states_partition tfsm) by A1, Th28, FINSEQ_4:91; :: thesis: verum