deffunc H₁( object ) -> set = (F . $1) " (A . $1);
ex f being ManySortedSet of I st
for i being object st i in I holds
f . i = H₁(i) from PBOOLE:sch 4();
hence ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = (F . i) " (A . i) ; :: thesis: verum