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