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:9
.= (r *' ) * (f . v,y) by Th30
.= (r *' ) * ((FunctionalFAF f,v) . y) by BILINEAR:9 ; :: thesis: verum