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 :: thesis: for x, y being Element of L holds f . (x,y) = g . (x,y)
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