deffunc H1( 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 = H1(x) ) ) from FUNCT_1:sch 3();
 then consider f being Function such that
A1: dom f = dom F and
A2: 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
A3: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
y = \\/ ((F . x),L) by A1, A2, A3;
hence y in the carrier of L ; :: thesis: verum
end;
then reconsider f = f as Function of (dom F), the carrier of L by A1, 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 A2; :: thesis: verum