deffunc H₁( object ) -> Element of the carrier of L = //\ ((F . $1),L);
ex f being Function st
( dom f = dom F & ( for x being object st x in dom F holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
then consider f being Function such that
A8: dom f = dom F and
A9: for x being object st x in dom F holds
f . x = //\ ((F . x),L) ;
rng f c= the carrier of L

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of L )
assume y in rng f ; :: thesis: y in the carrier of L
then consider x being object such that
A10: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
y = //\ ((F . x),L) by A8, A9, A10;
hence y in the carrier of L ; :: thesis: verum

end;

then reconsider f = f as Function of (dom F), the carrier of L by A8, FUNCT_2:2;
take f ; :: thesis: for x being object st x in dom F holds
f . x = //\ ((F . x),L)
thus for x being object st x in dom F holds
f . x = //\ ((F . x),L) by A9; :: thesis: verum