scheme :: SURREALR:sch 2
MonoFvSUniq{ F₁() -> Ordinal, F₂( Ordinal) -> set , F₃() -> Function-yielding c=-monotone Sequence, F₄() -> Function-yielding c=-monotone Sequence, F₅( object , Function-yielding c=-monotone Sequence) -> object } :

F₃() | F₁() = F₄() | F₁()

provided

A1: ( F₁() c= dom F₃() & F₁() c= dom F₄() ) and
A2: for A being Ordinal st A in F₁() holds
ex SA being ManySortedSet of F₂(A) st
( F₃() . A = SA & ( for o being object st o in F₂(A) holds
SA . o = F₅(o,(F₃() | A)) ) ) and
A3: for A being Ordinal st A in F₁() holds
ex SA being ManySortedSet of F₂(A) st
( F₄() . A = SA & ( for o being object st o in F₂(A) holds
SA . o = F₅(o,(F₄() | A)) ) )