deffunc H₁( Relation of ,, Element of NAT ) -> Relation of = $1 |^ A;
thus ex D being Relation of ex F being ManySortedSet of NAT st
( D = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of st R = F . i holds
F . (i + 1) = H₁(R,i) ) ) from PUA2MSS1:sch 1(); :: thesis: verum