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

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)

hence
f = g
by YELLOW_3:13; :: thesis: verumlet 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;thus f . (x,y) = x "\/" y by A3

.= g . (x,y) by A4 ; :: thesis: verum