deffunc H_{1}( 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_{1}(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

for i being object st i in I holds

f . i is Function of (A . i),(A . i)

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

consider f being Function such that

A1: ( dom f = I & ( for i being object st i in I holds

f . i = H

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

then reconsider f = f as ManySortedFunction of I by FUNCOP_1:def 6;
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;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

for i being object st i in I holds

f . i is Function of (A . i),(A . i)

proof

then reconsider f = f as ManySortedFunction of A,A by PBOOLE:def 15;
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;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

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