set lf = LQForm f;

thus LQForm f is additiveFAF :: thesis: LQForm f is homogeneousFAF

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 HAHNBAN1:def 8 :: thesis: for b_{1} being Element of the carrier of K holds (FunctionalFAF ((LQForm f),A)) . (b_{1} * w) = b_{1} * ((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 Th8

.= f . (v,(r * w)) by A2, Def20

.= r * (f . (v,w)) by Th32

.= r * ((LQForm f) . (A,w)) by A2, Def20

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

thus LQForm f is additiveFAF :: thesis: LQForm f is homogeneousFAF

proof

let A be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def 13 :: thesis: FunctionalFAF ((LQForm f),A) is homogeneous
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 Th8

.= f . (v,(w + t)) by A1, Def20

.= (f . (v,w)) + (f . (v,t)) by Th27

.= ((LQForm f) . (A,w)) + (f . (v,t)) by A1, Def20

.= ((LQForm f) . (A,w)) + ((LQForm f) . (A,t)) by A1, Def20

.= ((FunctionalFAF ((LQForm f),A)) . w) + ((LQForm f) . (A,t)) by Th8

.= ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t) by Th8 ; :: 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 Th8

.= f . (v,(w + t)) by A1, Def20

.= (f . (v,w)) + (f . (v,t)) by Th27

.= ((LQForm f) . (A,w)) + (f . (v,t)) by A1, Def20

.= ((LQForm f) . (A,w)) + ((LQForm f) . (A,t)) by A1, Def20

.= ((FunctionalFAF ((LQForm f),A)) . w) + ((LQForm f) . (A,t)) by Th8

.= ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t) by Th8 ; :: 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 HAHNBAN1:def 8 :: thesis: for b

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 Th8

.= f . (v,(r * w)) by A2, Def20

.= r * (f . (v,w)) by Th32

.= r * ((LQForm f) . (A,w)) by A2, Def20

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