scheme :: PUA2MSS1:sch 3
IndRelationUniq{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Nat, F₄() -> Relation of F₁(),F₂(), F₅( set , set ) -> Relation of F₁(),F₂() } :

for R1, R2 being Relation of F₁(),F₂() st ex F being ManySortedSet of NAT st
( R1 = F . F₃() & F . 0 = F₄() & ( for i being Nat
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) ) & ex F being ManySortedSet of NAT st
( R2 = F . F₃() & F . 0 = F₄() & ( for i being Nat
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) ) holds
R1 = R2