let f, g be Function of [:L,L:],L; :: thesis: ( ( for x, y being Element of L holds f . x,y = x "\/" y ) & ( for x, y being Element of L holds g . x,y = x "\/" y ) implies f = g )
assume that
A3: for x, y being Element of L holds f . x,y = x "\/" y and
A4: for x, y being Element of L holds g . x,y = x "\/" y ; :: thesis: f = g

now

let x, y be Element of L; :: thesis: f . x,y = g . x,y
thus f . x,y = x "\/" y by A3
.= g . x,y by A4 ; :: thesis: verum

end;

hence f = g by YELLOW_3:13; :: thesis: verum