for m being non zero Nat
for x, y, z, w being Element of REAL m
for i being Nat
for d, p, q, r being Real st 1 <= i & i <= m & |.(y - x).| < d & |.(z - x).| < d & p = (proj (i,m)) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
|.(w - x).| < d