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

| $RM = rng$ rostoucí úsekové ČRF }}

Dk ::

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

:: Popíšeme fci $f(i)$, která pro dané $i$ vrátí $i$-tý nejmenší prvek množiny $A$ (počítáme od 0, tj. první prvek je vrácen pro $i = 0$). :: Je-li $A$ konečná množina, není pro $i ≥ |A|$ hodnota $f(i)$ definována. Takto popsaná fce bude rostoucí i úseková. :: Intuitivní algoritmus, který bude počítat funkci $f(i)$ je jednoduchý: :: Najdi nejmenší prvek množiny $A$ a poté $i$-krát hledej nejmenší větší prvek. :: První cyklus while najde index nejmenšího (tedy 0-tého) prvku, který do množiny $A$ patří. :: Poté algoritmus $i$-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

ParseError: KaTeX parse error: Undefined control sequence: \[ at position 10: h(v) = μy\̲[̲χ_A(y) ≃ 1]

, všimněte si, že tato fce na svém parametru vůbec nezávisí, vždy najde nejmenší prvek množiny $A$. :: Funkci uvnitř cyklu for si definujeme jako ČRF

ParseError: KaTeX parse error: Undefined control sequence: \[ at position 16: g(i, u, v) = μz\̲[̲(z > u) ∧ χ_A(z…

. :: Funkce $g$ dostává jako druhou hodnotu hodnotu z rekurze, tedy aktuální hodnotu naposledy nalezeného prvku, následně hledá nejmenší prvek množiny $A$, který je větší než tento poslední nalezený prvek uložený v $z$. :: Pomocí primitivní rekurze odvodíme funkci $f' = R_2(h, g)$ a poté stačí položit $f(i) ≃ f' (i, i)$ :: (připomeňme si, že primitivní rekurze odvodí funkci alespoň dvou proměnných, proto funkci $f$ odvodíme takovouto oklikou).

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

:: Pokud $f$ není ORF, znamená to podle definice úsekové fce, že doména $f$ je konečná, a tedy je konečná i samotná množina $A$ a je tedy triviálně rekurzivní. :: Předpokládejme tedy, že $f$ je obecně rekurzivní, tedy všude definovaná fce, pro kterou platí, že $f(i)$ vrátí $i$-tý nejmenší prvek množiny $A$. :: Char. fci můžeme nyní spočítat jednoduchým způsobem. Množina $A$ je nekonečná, a proto musí obsahovat prvek, který je větší nebo roven $x$, ve skutečnosti platí, že $i$-tý prvek musí být větší nebo roven $i$, jinými slovy platí, že $i ≤ f(i)$. :: Proto ve skutečnosti stačí hledat $i ≤ x$ a mohli bychom se tedy obejít bez obecného cyklu while a nahradit jej cyklem for, toho využijeme při odvození fce $χ_A$. Definujme funkci

ParseError: KaTeX parse error: Undefined control sequence: \[ at position 14: g(x) = μi ≤ x\̲[̲f(i) ≥ x]

. :: Nyní platí, že $x ∈A$, právě když $x = f(g(x))$, přičemž rovnost je primitivně rekurzivní predikát, a proto je charakteristická fce $χ_A$ obecně rekurzivní. :: Pokud je $f$ dokonce PRF, dostaneme, že i χ_A je PRF, neboť omezená minimalizace použitá v odvození fce $g$ je primitivně rekurzivní. V každém případě je-li $f$ ORF, je ORF i $χ_A$ a $A$ je tedy RM.