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
ex k being Nat st
( k <= n & k -eq_states_partition tfsm is final )
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
ex k being Nat st
( k <= n & k -eq_states_partition tfsm is final )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: ( n + 1 = card the carrier of tfsm implies ex k being Nat st
( k <= n & k -eq_states_partition tfsm is final ) )
assume A1: n + 1 = card the carrier of tfsm ; :: thesis: ex k being Nat st
( k <= n & k -eq_states_partition tfsm is final )
take n ; :: thesis: ( n <= n & n -eq_states_partition tfsm is final )
thus n <= n ; :: thesis: n -eq_states_partition tfsm is final
n -eq_states_partition tfsm = (n + 1) -eq_states_partition tfsm by A1, Th35;
hence n -eq_states_partition tfsm is final by Th37; :: thesis: verum