theorem :: GEOMTRAP:29

for V being RealLinearSpace
for w, y, u, v being VECTOR of V holds PProJ (w,y,u,v) = PProJ (w,y,v,u) ;