deffunc H₁( set ) -> set = (X . $1) \/ (Y . $1);
consider f being Function such that
A1: dom f = I and
A2: for i being set st i in I holds
f . i = H₁(i) from FUNCT_1:sch 3();
f is ManySortedSet of I by A1, 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 A2; :: thesis: verum