let V be RealLinearSpace; :: thesis: for L being homogeneous Functional of V
for v being VECTOR of V holds L . (- v) = - (L . v)
let L be homogeneous Functional of V; :: thesis: for v being VECTOR of V holds L . (- v) = - (L . v)
let v be VECTOR of V; :: thesis: L . (- v) = - (L . v)
thus L . (- v) = L . ((- 1) * v) by RLVECT_1:16
.= (- 1) * (L . v) by Def3
.= - (L . v) ; :: thesis: verum