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