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

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)

hence
IT1 = IT2
by A1, BINOP_1:2; :: thesis: verumlet 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;thus IT1 . (p,q) = |.(p - q).| by A4

.= IT2 . (p,q) by A5 ; :: thesis: verum