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:13;
A3: 0.REAL 2 = 0. (TOP-REAL 2) by EUCLID:70;
then A4: P `1 = 0 by A1, Th32;
A5: P `2 = 0 by A1, A3, Th32;
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:12
.= sqrt (((z `1 ) ^2 ) + ((z `2 ) ^2 )) by A4, A5 ;
hence dist p,q = |.z.| by JGRAPH_1:47; :: thesis: verum