let x, y be Vector of V; :: according to HAHNBAN1:def 11 :: thesis: (0Functional V) . (x + y) = ((0Functional V) . x) + ((0Functional V) . y)
A1: (0Functional V) . x = 0. K by FUNCOP_1:13;
A2: (0Functional V) . y = 0. K by FUNCOP_1:13;
thus (0Functional V) . (x + y) = 0. K by FUNCOP_1:13
.= ((0Functional V) . x) + ((0Functional V) . y) by A1, A2, RLVECT_1:def 7 ; :: thesis: verum