let F1, F2 be Function of [:REAL ,REAL :],REAL ; :: thesis: ( ( for x, y being Element of REAL holds F1 . x,y = abs (x - y) ) & ( for x, y being Element of REAL holds F2 . x,y = abs (x - y) ) implies F1 = F2 )
assume that
A2: for x, y being Element of REAL holds F1 . x,y = abs (x - y) and
A3: for x, y being Element of REAL holds F2 . x,y = abs (x - y) ; :: thesis: F1 = F2
for x, y being Element of REAL holds F1 . x,y = F2 . x,y

proof

let x, y be Element of REAL ; :: thesis: F1 . x,y = F2 . x,y
thus F1 . x,y = abs (x - y) by A2
.= F2 . x,y by A3 ; :: thesis: verum

end;

hence F1 = F2 by BINOP_1:2; :: thesis: verum