scheme :: PUA2MSS1:sch 3
IndRelationUniq{ F1() -> non empty set , F2() -> non empty set , F3() -> Nat, F4() -> Relation of F1(),F2(), F5( set , set ) -> Relation of F1(),F2() } :
for R1, R2 being Relation of F1(),F2() st ex F being ManySortedSet of NAT st
( R1 = F . F3() & F . 0 = F4() & ( for i being Nat
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) ) & ex F being ManySortedSet of NAT st
( R2 = F . F3() & F . 0 = F4() & ( for i being Nat
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) ) holds
R1 = R2