let D1, D2 be Function of X,REAL ; :: thesis: ( ( 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 ; :: thesis: D1 = D2

now

let y be Element of X; :: thesis: D1 . y = D2 . y
D1 . y = f . x,y by A5;
hence D1 . y = D2 . y by A6; :: thesis: verum

end;

hence D1 = D2 by FUNCT_2:113; :: thesis: verum