deffunc H₁( 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₁(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