deffunc H₁( object ) -> set = [:(X . $1),(Y . $1):];
consider f being Function such that
A1: ( dom f = I & ( for i being object st i in I holds
f . i = H₁(i) ) ) 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 object st i in I holds
f . i = [:(X . i),(Y . i):]
thus for i being object st i in I holds
f . i = [:(X . i),(Y . i):] by A1; :: thesis: verum