(def-translation normed-spaces-to-rr 
    (source normed-linear-spaces)
    (target h-o-real-arithmetic)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs (uu rr))
    (constant-pairs (++ +)
		    (** *)
		    (v0 0)
		    (norm abs))
    (theory-interpretation-check using-simplification))

(def-translation mappings-on-interval-into-ns-to-rr 
    (source mappings-from-an-interval-to-a-normed-space)
    (target fixed-interval-theory)
    (core-translation normed-spaces-to-rr)
    (theory-interpretation-check using-simplification))

(def-transported-symbols (deriv primitive integral)
    (translation  mappings-on-interval-into-ns-to-rr)
    (renamer calculus-renamer)
    )

(def-theorem additivity-of-rr-derivative 
    "forall(f,g:[ii,rr],x:ii,
        #(rr%deriv(f,x)) and #(rr%deriv(g,x))
            implies 
          rr%deriv(lambda(x:ii,f(x)+g(x)),x)
          =rr%deriv(f,x)+rr%deriv(g,x));"
    (theory fixed-interval-theory)
    (proof
      (
        (apply-macete-with-minor-premises tr%additivity-of-deriv)
        simplify
        )))