deffunc H₁( set ) -> Element of bool (A . $1) = {} (A . $1);
consider f being Function such that
A1: ( dom f = I & ( for x being set st x in I holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: for i being set st i in I holds
f . i = {} (A . i)
thus for i being set st i in I holds
f . i = {} (A . i) by A1; :: thesis: verum