let y, x be real number ; :: thesis: for n being Element of 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 Element of 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 & e2 = p2 ) and
A2: e5 = y * p1 and
A3: e6 = y * p2 and
A4: dist e1,e2 < x and
A5: y <> 0 ; :: thesis: dist e5,e6 < (abs y) * x
reconsider f1 = e1, f2 = e2, f6 = e6 as Element of REAL n by A1, A3, EUCLID:25;
A6: REAL n = n -tuples_on REAL by EUCLID:def 1;
A7: dist e5,e6 = |.((y * f1) - f6).| by A1, A2, SPPOL_1:20
.= |.(y * (f1 - f2)).| by A1, A3, A6, Th7
.= (abs y) * |.(f1 - f2).| by EUCLID:14 ;
A8: dist e1,e2 = |.(f1 - f2).| by SPPOL_1:20;
0 < abs y by A5, COMPLEX1:133;
hence dist e5,e6 < (abs y) * x by A4, A7, A8, XREAL_1:70; :: thesis: verum