deffunc H₁( Element of L, Element of L) -> Element of the carrier of L = $1 "\/" $2;
A1: for x, y being Element of L holds H₁(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) = H₁(x,y) from YELLOW_3:sch 6(A1);
take f ; :: thesis: 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; :: thesis: verum