let w be Vector of V; :: according to BILINEAR:def 13 :: 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 8 :: 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 Th17
.= - ((FunctionalFAF (f,w)) . (a * v)) by HAHNBAN1:def 4
.= - (a * ((FunctionalFAF (f,w)) . v)) by HAHNBAN1:def 8
.= a * (- ((FunctionalFAF (f,w)) . v)) by VECTSP_1:8
.= a * ((- (FunctionalFAF (f,w))) . v) by HAHNBAN1:def 4
.= a * ((FunctionalFAF ((- f),w)) . v) by Th17 ; :: thesis: verum