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 :: thesis: for y being Element of X holds D1 . y = D2 . y

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 ; :: thesis: verum