deffunc H_{1}( 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_{1}(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

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

ex f being Function st

( dom f = dom F & ( for x being object st x in dom F holds

f . x = H

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

then reconsider f = f as Function of (dom F), the carrier of L by A8, FUNCT_2:2;
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;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

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