let IT1, IT2 be RealMap of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: ( ( for p, q being Point of (TOP-REAL n) holds IT1 . (p,q) = |.(p - q).| ) & ( for p, q being Point of (TOP-REAL n) holds IT2 . (p,q) = |.(p - q).| ) implies IT1 = IT2 )
assume that
A4: for p, q being Point of (TOP-REAL n) holds IT1 . (p,q) = |.(p - q).| and
A5: for p, q being Point of (TOP-REAL n) holds IT2 . (p,q) = |.(p - q).| ; :: thesis: IT1 = IT2

now :: thesis: for p, q being Point of (TOP-REAL n) holds IT1 . (p,q) = IT2 . (p,q)

let p, q be Point of (TOP-REAL n); :: thesis: IT1 . (p,q) = IT2 . (p,q)
thus IT1 . (p,q) = |.(p - q).| by A4
.= IT2 . (p,q) by A5 ; :: thesis: verum

end;

hence IT1 = IT2 by A1, BINOP_1:2; :: thesis: verum