scheme :: ALGSTR_4:sch 3
FuncRecursiveUniqu2{ F₁() -> non empty set , F₂( XFinSequence of F₁()) -> Element of F₁(), F₃() -> sequence of F₁(), F₄() -> sequence of F₁() } :

F₃() = F₄()

provided

A1: for n being Nat holds F₃() . n = F₂((F₃() | n)) and
A2: for n being Nat holds F₄() . n = F₂((F₄() | n))