deffunc H_{1}( 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_{1}(i)
from PBOOLE:sch 4();

hence ex b_{1} being ManySortedSet of the carrier of S st

for s being object st s in the carrier of S holds

b_{1} . s = { (a `1) where a is Element of rng t : a `2 = s }
; :: thesis: verum

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

hence ex b

for s being object st s in the carrier of S holds

b