for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for p, q, u, v, v9 being VECTOR of V
for A being Real st p,q,u,v are_DTr_wrt w,y & p <> q & A = ((PProJ (w,y,(p - q),(p + q))) - (2 * (PProJ (w,y,(p - q),u)))) * ((PProJ (w,y,(p - q),(p - q))) ") & v9 = u + (A * (p - q)) holds
v = v9