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
final_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
final_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 final_states_partition tfsm = n -eq_states_partition tfsm )
assume n + 1 = card the carrier of tfsm ; :: thesis: final_states_partition tfsm = n -eq_states_partition tfsm
then (n + 1) -eq_states_partition tfsm = n -eq_states_partition tfsm by Th35;
then n -eq_states_partition tfsm is final by Th37;
hence final_states_partition tfsm = n -eq_states_partition tfsm by Def15; :: thesis: verum