let X be RealUnitarySpace; :: thesis: for x, y being Point of X
for z, t being Point of (MetricSpaceNorm (RUSp2RNSp X)) st x = z & y = t holds
||.(x - y).|| = dist (z,t)
let x, y be Point of X; :: thesis: for z, t being Point of (MetricSpaceNorm (RUSp2RNSp X)) st x = z & y = t holds
||.(x - y).|| = dist (z,t)
let z, t be Point of (MetricSpaceNorm (RUSp2RNSp X)); :: thesis: ( x = z & y = t implies ||.(x - y).|| = dist (z,t) )
assume A1: ( x = z & y = t ) ; :: thesis: ||.(x - y).|| = dist (z,t)
reconsider x1 = x, y1 = y as Point of (RUSp2RNSp X) ;
thus ||.(x - y).|| = ||.(x1 - y1).|| by DUALSP04:3, DUALSP04:2
.= dist (z,t) by A1, NORMSP_2:def 1 ; :: thesis: verum