let k be Element of NAT ; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph st (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm holds
for i being Element of 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 of IAlph,OAlph st (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm holds
for i being Element of NAT st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: ( (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm implies for i being Element of 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 Element of NAT st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm
let i be Element of 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
assume A3: (i + 1) -eq_states_partition tfsm = i -eq_states_partition tfsm ; :: thesis: contradiction
consider d being Nat such that
A4: k = i + d by A2, NAT_1:10;
A5: k -eq_states_partition tfsm = i -eq_states_partition tfsm by A3, A4, Th46;
i <= k + 1 by A2, NAT_1:12;
then consider e being Nat such that
A6: k + 1 = i + e by NAT_1:10;
thus contradiction by A1, A3, A5, A6, Th46; :: thesis: verum