let D1, D2 be Function of X,REAL; ( ( for y being Element of X holds D1 . y = f . (x,y) ) & ( for y being Element of X holds D2 . y = f . (x,y) ) implies D1 = D2 )
assume that
A5:
for y being Element of X holds D1 . y = f . (x,y)
and
A6:
for y being Element of X holds D2 . y = f . (x,y)
; D1 = D2
hence
D1 = D2
; verum