set f = R --> (0. S);
let x, y be Element of R; :: according to VECTSP_1:def 19 :: thesis: (R --> (0. S)) . (x + y) = ((R --> (0. S)) . x) + ((R --> (0. S)) . y)
thus (R --> (0. S)) . (x + y) = 0. S by FUNCOP_1:7
.= (0. S) + (0. S) by RLVECT_1:def 4
.= (0. S) + ((R --> (0. S)) . y) by FUNCOP_1:7
.= ((R --> (0. S)) . x) + ((R --> (0. S)) . y) by FUNCOP_1:7 ; :: thesis: verum