let p, q be Point of (Euclid 2); :: thesis: for z being Point of (TOP-REAL 2) st p = 0.REAL 2 & q = z holds
dist (p,q) = |.z.|
let z be Point of (TOP-REAL 2); :: thesis: ( p = 0.REAL 2 & q = z implies dist (p,q) = |.z.| )
assume that
A1: p = 0.REAL 2 and
A2: q = z ; :: thesis: dist (p,q) = |.z.|
reconsider P = p as Point of (TOP-REAL 2) by TOPREAL3:8;
A3: 0.REAL 2 = 0. (TOP-REAL 2) by EUCLID:66;
then A4: P `1 = 0 by A1, Th22;
A5: P `2 = 0 by A1, A3, Th22;
dist (p,q) = (Pitag_dist 2) . (p,q) by METRIC_1:def 1
.= sqrt ((((P `1) - (z `1)) ^2) + (((P `2) - (z `2)) ^2)) by A2, TOPREAL3:7
.= sqrt (((z `1) ^2) + ((z `2) ^2)) by A4, A5 ;
hence dist (p,q) = |.z.| by JGRAPH_1:30; :: thesis: verum