deffunc H₁( 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₁(x) from FUNCT_2:sch 4(); :: thesis: verum