let x be Vector of V; :: according to HAHNBAN1:def 14 :: thesis: for r being Scalar of holds (0RFunctional V) . (r * x) = |.r.| * ((0RFunctional V) . x)
let r be Scalar of ; :: thesis: (0RFunctional V) . (r * x) = |.r.| * ((0RFunctional V) . x)
(0RFunctional V) . x = 0 by FUNCOP_1:7;
hence (0RFunctional V) . (r * x) = |.r.| * ((0RFunctional V) . x) by FUNCOP_1:7; :: thesis: verum