take (TOP-REAL n) --> (0. (TOP-REAL n)) ; :: thesis: ( (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous & (TOP-REAL n) --> (0. (TOP-REAL n)) is additive & (TOP-REAL n) --> (0. (TOP-REAL n)) is continuous )
thus ( (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous & (TOP-REAL n) --> (0. (TOP-REAL n)) is additive & (TOP-REAL n) --> (0. (TOP-REAL n)) is continuous ) ; :: thesis: verum