let w be Vector of V; :: according to BILINEAR:def 14 :: thesis: FunctionalFAF (- f),w is homogeneous
set Ffg = FunctionalFAF (- f),w;
set Ff = FunctionalFAF f,w;
let v be Vector of W; :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of K holds (FunctionalFAF (- f),w) . (b₁ * v) = b₁ * ((FunctionalFAF (- f),w) . v)
let a be Scalar of ; :: thesis: (FunctionalFAF (- f),w) . (a * v) = a * ((FunctionalFAF (- f),w) . v)
thus (FunctionalFAF (- f),w) . (a * v) = (- (FunctionalFAF f,w)) . (a * v) by Th18
.= - ((FunctionalFAF f,w) . (a * v)) by HAHNBAN1:def 7
.= - (a * ((FunctionalFAF f,w) . v)) by HAHNBAN1:def 12
.= a * (- ((FunctionalFAF f,w) . v)) by VECTSP_1:40
.= a * ((- (FunctionalFAF f,w)) . v) by HAHNBAN1:def 7
.= a * ((FunctionalFAF (- f),w) . v) by Th18 ; :: thesis: verum