set f = ZeroMap (V,W);
reconsider f = ZeroMap (V,W) as Function of V,W ;
take f ; :: thesis: ( f is additive & f is homogeneous )
thus ( f is additive & f is homogeneous ) ; :: thesis: verum