deffunc H_{1}( Element of L) -> Element of the carrier of L = "/\" (((uparrow $1) /\ the carrier of S),L);

thus ex f being Function of L,L st

for x being Element of L holds f . x = H_{1}(x)
from FUNCT_2:sch 4(); :: thesis: verum

thus ex f being Function of L,L st

for x being Element of L holds f . x = H