deffunc H₁( set ) -> set = (X . $1) /\ (Y . $1);
consider f being Function such that
A6: dom f = I and
A7: for i being set st i in I holds
f . i = H₁(i) from FUNCT_1:sch 3();
f is ManySortedSet of I by A6, PARTFUN1:def 4, RELAT_1:def 18;
hence ex b₁ being ManySortedSet of I st
for i being set st i in I holds
b₁ . i = (X . i) /\ (Y . i) by A7; :: thesis: verum