set lf = RQForm f;
thus RQForm f is additiveSAF :: thesis: RQForm f is homogeneousSAF

proof

let A be Vector of (VectQuot (W,(RKer f))); :: according to BILINEAR:def 12 :: thesis: FunctionalSAF ((RQForm f),A) is additive
set flf = FunctionalSAF ((RQForm f),A);
consider w being Vector of W such that
A3: A = w + (RKer f) by VECTSP10:22;
let v, t be Vector of V; :: according to VECTSP_1:def 19 :: thesis: (FunctionalSAF ((RQForm f),A)) . (v + t) = ((FunctionalSAF ((RQForm f),A)) . v) + ((FunctionalSAF ((RQForm f),A)) . t)
thus (FunctionalSAF ((RQForm f),A)) . (v + t) = (RQForm f) . ((v + t),A) by Th9
.= f . ((v + t),w) by A3, Def21
.= (f . (v,w)) + (f . (t,w)) by Th26
.= ((RQForm f) . (v,A)) + (f . (t,w)) by A3, Def21
.= ((RQForm f) . (v,A)) + ((RQForm f) . (t,A)) by A3, Def21
.= ((FunctionalSAF ((RQForm f),A)) . v) + ((RQForm f) . (t,A)) by Th9
.= ((FunctionalSAF ((RQForm f),A)) . v) + ((FunctionalSAF ((RQForm f),A)) . t) by Th9 ; :: thesis: verum

end;

let A be Vector of (VectQuot (W,(RKer f))); :: according to BILINEAR:def 14 :: thesis: FunctionalSAF ((RQForm f),A) is homogeneous
set flf = FunctionalSAF ((RQForm f),A);
consider w being Vector of W such that
A4: A = w + (RKer f) by VECTSP10:22;
let v be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for b₁ being Element of the carrier of K holds (FunctionalSAF ((RQForm f),A)) . (b₁ * v) = b₁ * ((FunctionalSAF ((RQForm f),A)) . v)
let r be Scalar of ; :: thesis: (FunctionalSAF ((RQForm f),A)) . (r * v) = r * ((FunctionalSAF ((RQForm f),A)) . v)
thus (FunctionalSAF ((RQForm f),A)) . (r * v) = (RQForm f) . ((r * v),A) by Th9
.= f . ((r * v),w) by A4, Def21
.= r * (f . (v,w)) by Th31
.= r * ((RQForm f) . (v,A)) by A4, Def21
.= r * ((FunctionalSAF ((RQForm f),A)) . v) by Th9 ; :: thesis: verum