theorem Th30: :: GEOMTRAP:30

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
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )