scheme :: ALGSTR_4:sch 1
FuncRecursiveUniq{ F₁( set ) -> set , F₂() -> Function, F₃() -> Function } :

F₂() = F₃()

provided

A1: ( dom F₂() = NAT & ( for n being Nat holds F₂() . n = F₁((F₂() | n)) ) ) and
A2: ( dom F₃() = NAT & ( for n being Nat holds F₃() . n = F₁((F₃() | n)) ) )