Description: If M follows Y in the R -sequence and if the procedure R
is single-valued, then every result of an application of the procedure
R to Y belongs to the R -sequence beginning with M or
precedes M in the R -sequence. Proposition 126 of Frege1879
p. 81. (Contributed by RP, 9-Jul-2020)(Proof modification is discouraged.)