let x be Vector of V; :: according to ZMODLAT1:def 22 :: thesis: for r being Scalar of holds (0FrFunctional V) . (r * x) = r * ((0FrFunctional V) . x)
let r be Scalar of ; :: thesis: (0FrFunctional V) . (r * x) = r * ((0FrFunctional V) . x)
A1: (0FrFunctional V) . x = 0. F_Real by FUNCOP_1:7;
thus (0FrFunctional V) . (r * x) = r * ((0FrFunctional V) . x) by A1, FUNCOP_1:7; :: thesis: verum