set lf = RQ*Form f;
thus RQ*Form f is additiveSAF :: thesis: RQ*Form f is homogeneousSAF

proof

let A be Vector of (VectQuot W,(RKer (f *' ))); :: according to BILINEAR:def 13 :: thesis: FunctionalSAF (RQ*Form f),A is additive
set flf = FunctionalSAF (RQ*Form f),A;
consider w being Vector of W such that
A3: A = w + (RKer (f *' )) by VECTSP10:23;
let v, t be Vector of V; :: according to GRCAT_1:def 13 :: thesis: (FunctionalSAF (RQ*Form f),A) . (v + t) = ((FunctionalSAF (RQ*Form f),A) . v) + ((FunctionalSAF (RQ*Form f),A) . t)
thus (FunctionalSAF (RQ*Form f),A) . (v + t) = (RQ*Form f) . (v + t),A by BILINEAR:10
.= f . (v + t),w by A3, Th62
.= (f . v,w) + (f . t,w) by BILINEAR:27
.= ((RQ*Form f) . v,A) + (f . t,w) by A3, Th62
.= ((RQ*Form f) . v,A) + ((RQ*Form f) . t,A) by A3, Th62
.= ((FunctionalSAF (RQ*Form f),A) . v) + ((RQ*Form f) . t,A) by BILINEAR:10
.= ((FunctionalSAF (RQ*Form f),A) . v) + ((FunctionalSAF (RQ*Form f),A) . t) by BILINEAR:10 ; :: thesis: verum

end;

let A be Vector of (VectQuot W,(RKer (f *' ))); :: according to BILINEAR:def 15 :: thesis: FunctionalSAF (RQ*Form f),A is homogeneous
set flf = FunctionalSAF (RQ*Form f),A;
consider w being Vector of W such that
A4: A = w + (RKer (f *' )) by VECTSP10:23;
let v be Vector of V; :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of F_Complex holds (FunctionalSAF (RQ*Form f),A) . (b₁ * v) = b₁ * ((FunctionalSAF (RQ*Form f),A) . v)
let r be Scalar of ; :: thesis: (FunctionalSAF (RQ*Form f),A) . (r * v) = r * ((FunctionalSAF (RQ*Form f),A) . v)
thus (FunctionalSAF (RQ*Form f),A) . (r * v) = (RQ*Form f) . (r * v),A by BILINEAR:10
.= f . (r * v),w by A4, Th62
.= r * (f . v,w) by BILINEAR:32
.= r * ((RQ*Form f) . v,A) by A4, Th62
.= r * ((FunctionalSAF (RQ*Form f),A) . v) by BILINEAR:10 ; :: thesis: verum