for G being RealNormSpace-Sequence
for x, y, z, w being Point of (product G)
for i being Element of dom G
for d being Real
for p, q, r being Point of (G . i) st ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
||.(w - x).|| < d