deffunc H₁( object ) -> Element of K19(K20((A . $1),(A . $1))) = id (A . $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;
for x being object st x in dom f holds
f . x is Function

proof

let x be object ; :: thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; :: thesis: f . x is Function
then f . x = id (A . x) by A1;
hence f . x is Function ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of I by FUNCOP_1:def 6;
for i being object st i in I holds
f . i is Function of (A . i),(A . i)

proof

let i be object ; :: thesis: ( i in I implies f . i is Function of (A . i),(A . i) )
assume i in I ; :: thesis: f . i is Function of (A . i),(A . i)
then f . i = id (A . i) by A1;
hence f . i is Function of (A . i),(A . i) ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of A,A by PBOOLE:def 15;
take f ; :: thesis: for i being set st i in I holds
f . i = id (A . i)
thus for i being set st i in I holds
f . i = id (A . i) by A1; :: thesis: verum