{{theorem | A je RM <math>\Leftrightarrow</math> je oborem hodnot nějaké rostoucí úsekové ČRF

| <math>RM = rng</math> rostoucí úsekové ČRF }}

Dk

<math> \Rightarrow\,\!</math>: Předpokládejme nejprve, že <math>A</math> je RM. To znamená, že její char. fce <math>χ_A(x)</math> je ORF.

Popíšeme fci <math>f(i)</math>, která pro dané <math>i</math> vrátí <math>i</math>-tý nejmenší prvek množiny <math>A</math> (počítáme od 0, tj. první prvek je vrácen pro <math>i = 0</math>).

Je-li <math>A</math> konečná množina, není pro <math>i ≥ |A|</math> hodnota <math>f(i)</math> definována. Takto popsaná fce bude rostoucí i úseková.

Intuitivní algoritmus, který bude počítat funkci <math>f(i)</math> je jednoduchý:

Najdi nejmenší prvek množiny <math>A</math> a poté <math>i</math>-krát hledej nejmenší větší prvek.

První cyklus while najde index nejmenšího (tedy 0-tého) prvku, který do množiny <math>A</math> patří.

Poté algoritmus <math>i</math>-krát opakuje hledání následujícího prvku.

Hledání následujícího prvku je obsaženo v druhém cyklu while.

První inicializační cyklus si definujeme jako ČRF <math>h(v) = μy[χ_A(y) ≃ 1]</math>, všimněte si, že tato fce na svém parametru vůbec nezávisí, vždy najde nejmenší prvek množiny <math>A</math>.

Funkci uvnitř cyklu for si definujeme jako ČRF <math>g(i, u, v) = μz[(z > u) ∧ χ_A(z) ≃ 1]</math>.

Funkce <math>g</math> dostává jako druhou hodnotu hodnotu z rekurze, tedy aktuální hodnotu naposledy nalezeného prvku, následně hledá nejmenší prvek množiny <math>A</math>, který je větší než tento poslední nalezený prvek uložený v <math>z</math>.

Pomocí primitivní rekurze odvodíme funkci <math>f' = R_2(h, g)</math> a poté stačí položit <math>f(i) ≃ f' (i, i)</math>

(připomeňme si, že primitivní rekurze odvodí funkci alespoň dvou proměnných, proto funkci <math>f</math> odvodíme takovouto oklikou).

<math> \Leftarrow\,\!</math>: Nyní předpokládejme, že <math>A = rng f</math>, kde <math>f</math> je rostoucí úseková ČRF.

Pokud <math>f</math> není ORF, znamená to podle definice úsekové fce, že doména <math>f</math> je konečná, a tedy je konečná i samotná množina <math>A</math> a je tedy triviálně rekurzivní.

Předpokládejme tedy, že <math>f</math> je obecně rekurzivní, tedy všude definovaná fce, pro kterou platí, že <math>f(i)</math> vrátí <math>i</math>-tý nejmenší prvek množiny <math>A</math>.

Char. fci můžeme nyní spočítat jednoduchým způsobem. Množina <math>A</math> je nekonečná, a proto musí obsahovat prvek, který je větší nebo roven <math>x</math>, ve skutečnosti platí, že <math>i</math>-tý prvek musí být větší nebo roven <math>i</math>, jinými slovy platí, že <math>i ≤ f(i)</math>.

Proto ve skutečnosti stačí hledat <math>i ≤ x</math> a mohli bychom se tedy obejít bez obecného cyklu while a nahradit jej cyklem for, toho využijeme při odvození fce <math>χ_A</math>. Definujme funkci <math>g(x) = μi ≤ x[f(i) ≥ x]</math>.

Nyní platí, že <math>x ∈A</math>, právě když <math>x = f(g(x))</math>, přičemž rovnost je primitivně rekurzivní predikát, a proto je charakteristická fce <math>χ_A</math> obecně rekurzivní.

Pokud je <math>f</math> dokonce PRF, dostaneme, že i χ_A je PRF, neboť omezená minimalizace použitá v odvození fce <math>g</math> je primitivně rekurzivní. V každém případě je-li <math>f</math> ORF, je ORF i <math>χ_A</math> a <math>A</math> je tedy RM.