set lf = LQForm f;

thus LQForm f is additiveFAF :: thesis: LQForm f is cmplxhomogeneousFAF

set flf = FunctionalFAF ((LQForm f),A);

consider v being Vector of V such that

A2: A = v + (LKer f) by VECTSP10:22;

let w be Vector of W; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (FunctionalFAF ((LQForm f),A)) . (a * w) = (a *') * ((FunctionalFAF ((LQForm f),A)) . w)

let r be Scalar of ; :: thesis: (FunctionalFAF ((LQForm f),A)) . (r * w) = (r *') * ((FunctionalFAF ((LQForm f),A)) . w)

thus (FunctionalFAF ((LQForm f),A)) . (r * w) = (LQForm f) . (A,(r * w)) by BILINEAR:8

.= f . (v,(r * w)) by A2, BILINEAR:def 20

.= (r *') * (f . (v,w)) by Th27

.= (r *') * ((LQForm f) . (A,w)) by A2, BILINEAR:def 20

.= (r *') * ((FunctionalFAF ((LQForm f),A)) . w) by BILINEAR:8 ; :: thesis: verum

thus LQForm f is additiveFAF :: thesis: LQForm f is cmplxhomogeneousFAF

proof

let A be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def 4 :: thesis: FunctionalFAF ((LQForm f),A) is cmplxhomogeneous
let A be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def 11 :: thesis: FunctionalFAF ((LQForm f),A) is additive

set flf = FunctionalFAF ((LQForm f),A);

consider v being Vector of V such that

A1: A = v + (LKer f) by VECTSP10:22;

let w, t be Vector of W; :: according to VECTSP_1:def 19 :: thesis: (FunctionalFAF ((LQForm f),A)) . (w + t) = ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t)

thus (FunctionalFAF ((LQForm f),A)) . (w + t) = (LQForm f) . (A,(w + t)) by BILINEAR:8

.= f . (v,(w + t)) by A1, BILINEAR:def 20

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

.= ((LQForm f) . (A,w)) + (f . (v,t)) by A1, BILINEAR:def 20

.= ((LQForm f) . (A,w)) + ((LQForm f) . (A,t)) by A1, BILINEAR:def 20

.= ((FunctionalFAF ((LQForm f),A)) . w) + ((LQForm f) . (A,t)) by BILINEAR:8

.= ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t) by BILINEAR:8 ; :: thesis: verum

end;set flf = FunctionalFAF ((LQForm f),A);

consider v being Vector of V such that

A1: A = v + (LKer f) by VECTSP10:22;

let w, t be Vector of W; :: according to VECTSP_1:def 19 :: thesis: (FunctionalFAF ((LQForm f),A)) . (w + t) = ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t)

thus (FunctionalFAF ((LQForm f),A)) . (w + t) = (LQForm f) . (A,(w + t)) by BILINEAR:8

.= f . (v,(w + t)) by A1, BILINEAR:def 20

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

.= ((LQForm f) . (A,w)) + (f . (v,t)) by A1, BILINEAR:def 20

.= ((LQForm f) . (A,w)) + ((LQForm f) . (A,t)) by A1, BILINEAR:def 20

.= ((FunctionalFAF ((LQForm f),A)) . w) + ((LQForm f) . (A,t)) by BILINEAR:8

.= ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t) by BILINEAR:8 ; :: thesis: verum

set flf = FunctionalFAF ((LQForm f),A);

consider v being Vector of V such that

A2: A = v + (LKer f) by VECTSP10:22;

let w be Vector of W; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (FunctionalFAF ((LQForm f),A)) . (a * w) = (a *') * ((FunctionalFAF ((LQForm f),A)) . w)

let r be Scalar of ; :: thesis: (FunctionalFAF ((LQForm f),A)) . (r * w) = (r *') * ((FunctionalFAF ((LQForm f),A)) . w)

thus (FunctionalFAF ((LQForm f),A)) . (r * w) = (LQForm f) . (A,(r * w)) by BILINEAR:8

.= f . (v,(r * w)) by A2, BILINEAR:def 20

.= (r *') * (f . (v,w)) by Th27

.= (r *') * ((LQForm f) . (A,w)) by A2, BILINEAR:def 20

.= (r *') * ((FunctionalFAF ((LQForm f),A)) . w) by BILINEAR:8 ; :: thesis: verum