let y, x be real number ; :: thesis: for n being Nat
for e1, e2, e5, e6 being Point of (Euclid n)
for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds
dist (e5,e6) < (abs y) * x
let n be Nat; :: thesis: for e1, e2, e5, e6 being Point of (Euclid n)
for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds
dist (e5,e6) < (abs y) * x
let e1, e2, e5, e6 be Point of (Euclid n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds
dist (e5,e6) < (abs y) * x
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 implies dist (e5,e6) < (abs y) * x )
assume that
A1: e1 = p1 and
A2: e2 = p2 and
A3: e5 = y * p1 and
A4: e6 = y * p2 and
A5: dist (e1,e2) < x and
A6: y <> 0 ; :: thesis: dist (e5,e6) < (abs y) * x
reconsider f1 = e1, f2 = e2, f5 = e5, f6 = e6 as Element of REAL n by A1, A2, A3, A4, EUCLID:22;
A7: n in NAT by ORDINAL1:def 12;
then A8: dist (e1,e2) = |.(f1 - f2).| by SPPOL_1:5;
A9: 0 < abs y by A6, COMPLEX1:47;
dist (e5,e6) = |.(f5 - f6).| by A7, SPPOL_1:5
.= |.((y * f1) - f6).| by A1, A3, EUCLID:65
.= |.((y * f1) - (y * f2)).| by A2, A4, EUCLID:65
.= |.(y * (f1 - f2)).| by Th7
.= (abs y) * |.(f1 - f2).| by EUCLID:11 ;
hence dist (e5,e6) < (abs y) * x by A5, A8, A9, XREAL_1:68; :: thesis: verum