let x, y be Vector of V; :: according to VECTSP_1:def 19 :: thesis: (0FrFunctional V) . (x + y) = ((0FrFunctional V) . x) + ((0FrFunctional V) . y)
A1: ( (0FrFunctional V) . x = 0. F_Real & (0FrFunctional V) . y = 0. F_Real ) by FUNCOP_1:7;
thus (0FrFunctional V) . (x + y) = ((0FrFunctional V) . x) + ((0FrFunctional V) . y) by A1, FUNCOP_1:7; :: thesis: verum