exp_term: THEORY
BEGIN

  IMPORTING reals@factorial

  a:   VAR real
  n0a: VAR nzreal
  n,m:   VAR nat
  i:   VAR int
  epsilon: VAR posreal
  f:   VAR [nat->real]

  exp_term(a)(n):real = IF n = 0 THEN 1 ELSE a^n/factorial(n) ENDIF

  exp_term_power: LEMMA a /= 0 IMPLIES
                                 abs(exp_term(a)(m*n)) <= abs(exp_term(a)(n))^m
  exp_term_decr:  LEMMA a /= 0 AND abs(a) < n+1 IMPLIES
                                 abs(exp_term(a)(n+1)) < abs(exp_term(a)(n))

  tends_to_0?(f):bool = FORALL epsilon: EXISTS n:
                                FORALL i: i >= n IMPLIES abs(f(i)) < epsilon

  exp_tends_to_0: LEMMA tends_to_0?(exp_term(n0a))

END exp_term