let x, y be Vector of V; :: according to HAHNBAN1:def 17 :: thesis: (0RFunctional V) . (x + y) = ((0RFunctional V) . x) + ((0RFunctional V) . y)
A1: (0RFunctional V) . x = 0 by FUNCOP_1:13;
(0RFunctional V) . y = 0 by FUNCOP_1:13;
hence (0RFunctional V) . (x + y) = ((0RFunctional V) . x) + ((0RFunctional V) . y) by A1, FUNCOP_1:13; :: thesis: verum