deffunc H₁( object ) -> set = { (a `1) where a is Element of rng t : a `2 = $1 } ;
ex f being ManySortedSet of the carrier of S st
for i being object st i in the carrier of S holds
f . i = H₁(i) from PBOOLE:sch 4();
hence ex b₁ being ManySortedSet of the carrier of S st
for s being object st s in the carrier of S holds
b₁ . s = { (a `1) where a is Element of rng t : a `2 = s } ; :: thesis: verum