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

let r be Scalar of ; :: thesis: (FunctionalFAF (f,v)) . (r * y) = (r *') * ((FunctionalFAF (f,v)) . y)

set F = FunctionalFAF (f,v);

thus (FunctionalFAF (f,v)) . (r * y) = f . (v,(r * y)) by BILINEAR:8

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

.= (r *') * ((FunctionalFAF (f,v)) . y) by BILINEAR:8 ; :: thesis: verum

let r be Scalar of ; :: thesis: (FunctionalFAF (f,v)) . (r * y) = (r *') * ((FunctionalFAF (f,v)) . y)

set F = FunctionalFAF (f,v);

thus (FunctionalFAF (f,v)) . (r * y) = f . (v,(r * y)) by BILINEAR:8

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

.= (r *') * ((FunctionalFAF (f,v)) . y) by BILINEAR:8 ; :: thesis: verum