set lf = RQ*Form f;

thus RQ*Form f is additiveSAF :: thesis: RQ*Form f is homogeneousSAF

set flf = FunctionalSAF ((RQ*Form 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_{1} being Element of the carrier of F_Complex holds (FunctionalSAF ((RQ*Form f),A)) . (b_{1} * v) = b_{1} * ((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:9

.= f . ((r * v),w) by A4, Th59

.= r * (f . (v,w)) by BILINEAR:31

.= r * ((RQ*Form f) . (v,A)) by A4, Th59

.= r * ((FunctionalSAF ((RQ*Form f),A)) . v) by BILINEAR:9 ; :: thesis: verum

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 14 :: thesis: FunctionalSAF ((RQ*Form f),A) is homogeneous
let A be Vector of (VectQuot (W,(RKer (f *')))); :: according to BILINEAR:def 12 :: 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:22;

let v, t be Vector of V; :: according to VECTSP_1:def 19 :: 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:9

.= f . ((v + t),w) by A3, Th59

.= (f . (v,w)) + (f . (t,w)) by BILINEAR:26

.= ((RQ*Form f) . (v,A)) + (f . (t,w)) by A3, Th59

.= ((RQ*Form f) . (v,A)) + ((RQ*Form f) . (t,A)) by A3, Th59

.= ((FunctionalSAF ((RQ*Form f),A)) . v) + ((RQ*Form f) . (t,A)) by BILINEAR:9

.= ((FunctionalSAF ((RQ*Form f),A)) . v) + ((FunctionalSAF ((RQ*Form f),A)) . t) by BILINEAR:9 ; :: thesis: verum

end;set flf = FunctionalSAF ((RQ*Form 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 ((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:9

.= f . ((v + t),w) by A3, Th59

.= (f . (v,w)) + (f . (t,w)) by BILINEAR:26

.= ((RQ*Form f) . (v,A)) + (f . (t,w)) by A3, Th59

.= ((RQ*Form f) . (v,A)) + ((RQ*Form f) . (t,A)) by A3, Th59

.= ((FunctionalSAF ((RQ*Form f),A)) . v) + ((RQ*Form f) . (t,A)) by BILINEAR:9

.= ((FunctionalSAF ((RQ*Form f),A)) . v) + ((FunctionalSAF ((RQ*Form f),A)) . t) by BILINEAR:9 ; :: thesis: verum

set flf = FunctionalSAF ((RQ*Form 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

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:9

.= f . ((r * v),w) by A4, Th59

.= r * (f . (v,w)) by BILINEAR:31

.= r * ((RQ*Form f) . (v,A)) by A4, Th59

.= r * ((FunctionalSAF ((RQ*Form f),A)) . v) by BILINEAR:9 ; :: thesis: verum