:: deftheorem Def5 defines pr2 GEOMTRAP:def 5 :
for V being RealLinearSpace
for w, y, u being VECTOR of V st Gen w,y holds
for b₅ being Real holds
( b₅ = pr2 (w,y,u) iff ex a being Real st u = (a * w) + (b₅ * y) );