let n be Nat; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph st n + 1 = card the carrier of tfsm holds
(n + 1) -eq_states_partition tfsm = n -eq_states_partition tfsm
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM over IAlph,OAlph st n + 1 = card the carrier of tfsm holds
(n + 1) -eq_states_partition tfsm = n -eq_states_partition tfsm
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: ( n + 1 = card the carrier of tfsm implies (n + 1) -eq_states_partition tfsm = n -eq_states_partition tfsm )
assume A1: n + 1 = card the carrier of tfsm ; :: thesis: (n + 1) -eq_states_partition tfsm = n -eq_states_partition tfsm
defpred S1[ Nat] means ( $1 <= n + 1 implies card ($1 -eq_states_partition tfsm) > $1 );
assume A2: (n + 1) -eq_states_partition tfsm <> n -eq_states_partition tfsm ; :: thesis: contradiction
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: ( k <= n + 1 implies card (k -eq_states_partition tfsm) > k ) ; :: thesis: S1[k + 1]
assume A5: k + 1 <= n + 1 ; :: thesis: card ((k + 1) -eq_states_partition tfsm) > k + 1
then k <= n by XREAL_1:6;
then A6: (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm by A2, Th31;
k + 1 <= card (k -eq_states_partition tfsm) by A4, A5, NAT_1:13;
hence card ((k + 1) -eq_states_partition tfsm) > k + 1 by A6, Th32, XXREAL_0:2; :: thesis: verum
end;
A7: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A7, A3);
 then card ((n + 1) -eq_states_partition tfsm) > n + 1 ;
hence contradiction by A1, FINSEQ_4:88; :: thesis: verum