deffunc H₁( object ) -> Element of D = B "**" (F . $1);
consider f being Function such that
A1: ( dom f = dom F & ( for x being object st x in dom F holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
rng f c= D

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in D )
assume A2: y in rng f ; :: thesis: y in D
consider x being object such that
A3: ( x in dom f & f . x = y ) by A2, FUNCT_1:def 3;
y = B "**" (F . x) by A3, A1;
hence y in D ; :: thesis: verum

end;

then reconsider f = f as Function of (dom F),D by A1, FUNCT_2:2;
take f ; :: thesis: for x being object st x in dom F holds
f . x = B "**" (F . x)
thus for x being object st x in dom F holds
f . x = B "**" (F . x) by A1; :: thesis: verum