scheme :: PRE_CIRC:sch 3
LambdaRecCorrD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( Nat, Element of F₁()) -> Element of F₁() } :

( ex f being sequence of F₁() st
( f . 0 = F₂() & ( for i being Nat holds f . (i + 1) = F₃(i,(f . i)) ) ) & ( for f1, f2 being sequence of F₁() st f1 . 0 = F₂() & ( for i being Nat holds f1 . (i + 1) = F₃(i,(f1 . i)) ) & f2 . 0 = F₂() & ( for i being Nat holds f2 . (i + 1) = F₃(i,(f2 . i)) ) holds
f1 = f2 ) )