thus ex M being ManySortedSet of I st
for i being object st i in I holds
M . i = H₁(i) from PBOOLE:sch 4(); :: thesis: verum