set f = FuncZero (([#] V),W);
reconsider f = FuncZero (([#] V),W) as Function of V,W ;
A1: for x, y being Vector of V holds f . (x + y) = (f . x) + (f . y)

proof

let x, y be Vector of V; :: thesis: f . (x + y) = (f . x) + (f . y)
A2: f . y = 0. W by FUNCOP_1:7;
( f . (x + y) = 0. W & f . x = 0. W ) by FUNCOP_1:7;
hence f . (x + y) = (f . x) + (f . y) by A2, RLVECT_1:def 4; :: thesis: verum

end;

take f ; :: thesis: ( f is additive & f is homogeneous )
for a being Element of F
for x being Element of V holds f . (a * x) = a * (f . x)

proof

let a be Element of F; :: thesis: for x being Element of V holds f . (a * x) = a * (f . x)
let x be Element of V; :: thesis: f . (a * x) = a * (f . x)
( f . (a * x) = 0. W & f . x = 0. W ) by FUNCOP_1:7;
hence f . (a * x) = a * (f . x) by VECTSP_1:14; :: thesis: verum

end;

hence ( f is additive & f is homogeneous ) by A1, GRCAT_1:def 8, MOD_2:def 2; :: thesis: verum