:: deftheorem defines PProJ GEOMTRAP:def 6 :
for V being RealLinearSpace
for w, y, u, v being VECTOR of V holds PProJ (w,y,u,v) = ((pr1 (w,y,u)) * (pr1 (w,y,v))) + ((pr2 (w,y,u)) * (pr2 (w,y,v)));