proposition: Lemma Lim_areIso : AreBij0'' PhiCone_1_map PhiCone_map.
proof: Proof. unfold AreBij0'' in |- *; split. intro f; simpl in |- *; unfold PhiCone_fun in |- *. apply Sym; apply (Prf_limit2 l). unfold Limit_eq, PhiCone_1_fun in |- *; simpl in |- *. intro i; apply Refl. intro tau; simpl in |- *; unfold Equal_NT in |- *. unfold PhiCone_1_fun, PhiCone_fun in |- *; simpl in |- *. intro i; unfold PhiCone_1_fun_tau in |- *. apply (Prf_limit1 l tau i). Qed.
imports: SET Limit Map0_dup1