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

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

hence
D1 = D2
; :: thesis: verumlet 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;D1 . y = f . (x,y) by A5;

hence D1 . y = D2 . y by A6; :: thesis: verum