let f, g be Function of [:L,L:],L; ( ( 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
; f = g
now for x, y being Element of L holds f . (x,y) = g . (x,y)let x,
y be
Element of
L;
f . (x,y) = g . (x,y)thus f . (
x,
y) =
x "\/" y
by A3
.=
g . (
x,
y)
by A4
;
verum end;
hence
f = g
by YELLOW_3:13; verum