let x, y be Real; :: thesis: for A being SubSpace of RealSpace
for p, q being Point of A st x = p & y = q holds
dist (p,q) = |.(x - y).|
let A be SubSpace of RealSpace ; :: thesis: for p, q being Point of A st x = p & y = q holds
dist (p,q) = |.(x - y).|
let p, q be Point of A; :: thesis: ( x = p & y = q implies dist (p,q) = |.(x - y).| )
assume A1: ( x = p & y = q ) ; :: thesis: dist (p,q) = |.(x - y).|
thus dist (p,q) = the distance of A . (p,q) by METRIC_1:def 1
.= real_dist . (x,y) by A1, METRIC_1:def 13, TOPMETR:def 1
.= |.(x - y).| by METRIC_1:def 12 ; :: thesis: verum