theorem Th34: :: GEOMTRAP:34

for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, v, v1 being VECTOR of V holds 2 * (PProJ (w,y,u,(v # v1))) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1))