take (REAL m) --> (0* n) ; :: thesis: ( (REAL m) --> (0* n) is additive & (REAL m) --> (0* n) is homogeneous )
thus ( (REAL m) --> (0* n) is additive & (REAL m) --> (0* n) is homogeneous ) ; :: thesis: verum