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