let k be Nat; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph st (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm holds
for i being Nat st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph st (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm holds
for i being Nat st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: ( (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm implies for i being Nat st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm )
assume A1: (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm ; :: thesis: for i being Nat st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm
let i be Nat; :: thesis: ( i <= k implies (i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm )
assume A2: i <= k ; :: thesis: (i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm
A3: ex e being Nat st k + 1 = i + e by A2, NAT_1:10, NAT_1:12;
assume A4: (i + 1) -eq_states_partition tfsm = i -eq_states_partition tfsm ; :: thesis: contradiction
ex d being Nat st k = i + d by A2, NAT_1:10;
then k -eq_states_partition tfsm = i -eq_states_partition tfsm by A4, Th29;
hence contradiction by A1, A4, A3, Th29; :: thesis: verum