Who introduced nondeterministic M-automata, and proved that the finite ones recognize the rational sets over M?
According to J. Sakarovich, Elements of Automata Theory, p. 372, 


  It seems that the result appears for the first time in [1]; hidden in a footnote of this seminal but difficult article, it was then given many statements, usually in special cases. 


[1] C. C. Elgot and J. E. Mezei, On relations defined by generalized finite automata, IBM J. Res. and Develop., vol. 9 (1965), 47–68.

A full proof was also given in S. Eilenberg, Automata, Languages and Machines, vol. A, Academic Press, 1974.