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