proposition: Lemma Exp_Log_inv : Feq (openl [0]) (Expon[o]Logarithm) FId.
proof: Proof. apply eq_imp_Feq. red in |- *; intros x H. simpl in H; exists H; apply Exp_domain. Included. intros x H Hx Hx'; simpl in |- *. astepr (Exp (Log x H)). unfold Log in |- *; simpl in |- *; algebra. Qed.
imports: CoRN.transc.TaylorSeries