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

now

let p, q be Point of ; :: 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