take ZeroMap (M,N) ; :: thesis: ( ZeroMap (M,N) is additive & ZeroMap (M,N) is homogeneous )
thus ( ZeroMap (M,N) is additive & ZeroMap (M,N) is homogeneous ) ; :: thesis: verum