Description: If X is a result of an application of the single-valued procedure
R to Y , then every result of an application of the procedure
R to Y belongs to the R -sequence beginning with X .
Proposition 122 of Frege1879 p. 79. (Contributed by RP, 8-Jul-2020)(Proof modification is discouraged.)