deffunc H1( Element of L, Element of L) -> Element of the carrier of L = $1 "/\" $2;
A1:
for x, y being Element of L holds H1(x,y) is Element of L
;
consider f being Function of [:L,L:],L such that
A2:
for x, y being Element of L holds f . (x,y) = H1(x,y)
from YELLOW_3:sch 6(A1);
take
f
; for x, y being Element of L holds f . (x,y) = x "/\" y
thus
for x, y being Element of L holds f . (x,y) = x "/\" y
by A2; verum