deffunc H_{1}( object ) -> Element of bool [:[:X,(f . $1):],(f . $1):] = pr2 (X,(f . $1));

consider g being Function such that

A1: ( dom g = dom f & ( for x being object st x in dom f holds

g . x = H_{1}(x) ) )
from FUNCT_1:sch 3();

take g ; :: thesis: ( dom g = dom f & ( for i being set st i in dom f holds

g . i is Function of [:X,(f . i):],(f . i) ) )

thus dom g = dom f by A1; :: thesis: for i being set st i in dom f holds

g . i is Function of [:X,(f . i):],(f . i)

let i be set ; :: thesis: ( i in dom f implies g . i is Function of [:X,(f . i):],(f . i) )

assume i in dom f ; :: thesis: g . i is Function of [:X,(f . i):],(f . i)

then g . i = pr2 (X,(f . i)) by A1;

hence g . i is Function of [:X,(f . i):],(f . i) ; :: thesis: verum

consider g being Function such that

A1: ( dom g = dom f & ( for x being object st x in dom f holds

g . x = H

take g ; :: thesis: ( dom g = dom f & ( for i being set st i in dom f holds

g . i is Function of [:X,(f . i):],(f . i) ) )

thus dom g = dom f by A1; :: thesis: for i being set st i in dom f holds

g . i is Function of [:X,(f . i):],(f . i)

let i be set ; :: thesis: ( i in dom f implies g . i is Function of [:X,(f . i):],(f . i) )

assume i in dom f ; :: thesis: g . i is Function of [:X,(f . i):],(f . i)

then g . i = pr2 (X,(f . i)) by A1;

hence g . i is Function of [:X,(f . i):],(f . i) ; :: thesis: verum