deffunc H₁( Relation of the carrier of A, the carrier of A, Nat) -> Relation of the carrier of A = $1 |^ A;
thus for D1, D2 being Relation of the carrier of A st ex F being ManySortedSet of NAT st
( D1 = 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) ) ) & ex F being ManySortedSet of NAT st
( D2 = 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) ) ) holds
D1 = D2 from PUA2MSS1:sch 3(); :: thesis: verum