scheme :: RECDEF_1:sch 11
DefRec{ F₁() -> object , F₂() -> Nat, P₁[ object , object , object ] } :

( ex y being set ex f being Function st
( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )

provided

A1: for n being Nat
for x being set ex y being set st P₁[n,x,y] and
A2: for n being Nat
for x, y1, y2 being set st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2