2. in : |R|
IdLnk
3. out : |R|
IdLnk
4.
i:|R|.
4. R(source(in(i))) & R(destination(out(i)))
4. & source(out(i)) = i
4. & & destination(in(i)) = i
4. & & in(destination(out(i))) = out(i)
4. & & out(source(in(i))) = in(i)
5.
i,j:|R|. 
k:
. 
x.destination(out(x))^k(i) = j
6. i : Id
7. R(i)
8. k :
9. (
x.destination(out(x))) 
|R||R|
10. i@0 : |R|
11.
i@0 = i
12. j : |R|
13. n :
14.
n1:.
14. n1<n
14.
14.
x.destination(out(x))^n1(i) = j (m:k. x.destination(out(x))^m(i) = j)
15.
x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j
16.
n<k
17. f : |R|
|R|
18. (
x.destination(out(x))) = f
19. f^k(i) = i
20. z : Id
21. z = i
R(z)
