scheme :: ORDINAL2:sch 19
RecUn{ F₁() -> set , F₂() -> Function, F₃() -> Function, P₁[ set , set , set ] } :

F₂() = F₃()

provided

A1: dom F₂() = omega and
A2: F₂() . 0 = F₁() and
A3: for n being Nat holds P₁[n,F₂() . n,F₂() . (succ n)] and
A4: dom F₃() = omega and
A5: F₃() . 0 = F₁() and
A6: for n being Nat holds P₁[n,F₃() . n,F₃() . (succ n)] and
A7: for n being Nat
for x, y1, y2 being set st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2