let F1, F2 be Function of [:REAL,REAL:],REAL; :: thesis: ( ( for x, y being Real holds F1 . (x,y) = |.(x - y).| ) & ( for x, y being Real holds F2 . (x,y) = |.(x - y).| ) implies F1 = F2 )

assume that

A2: for x, y being Real holds F1 . (x,y) = |.(x - y).| and

A3: for x, y being Real holds F2 . (x,y) = |.(x - y).| ; :: thesis: F1 = F2

for x, y being Element of REAL holds F1 . (x,y) = F2 . (x,y)

assume that

A2: for x, y being Real holds F1 . (x,y) = |.(x - y).| and

A3: for x, y being Real holds F2 . (x,y) = |.(x - y).| ; :: thesis: F1 = F2

for x, y being Element of REAL holds F1 . (x,y) = F2 . (x,y)

proof

hence
F1 = F2
; :: thesis: verum
let x, y be Element of REAL ; :: thesis: F1 . (x,y) = F2 . (x,y)

thus F1 . (x,y) = |.(x - y).| by A2

.= F2 . (x,y) by A3 ; :: thesis: verum

end;thus F1 . (x,y) = |.(x - y).| by A2

.= F2 . (x,y) by A3 ; :: thesis: verum