proposition: Lemma continuous_I_power : forall F G a b Hab, Continuous_I Hab F -> Continuous_I Hab G -> positive_fun (compact a b Hab) F -> Continuous_I Hab (F{!}G).
proof: Proof. intros. apply (Int_Continuous (clcr a b) Hab). apply Continuous_power. auto. apply Continuous_Int with Hab Hab; auto. apply Continuous_Int with Hab Hab; auto. Qed.
imports: CoRN.transc.Exponential