(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(***************************************************************************)
(* File: axs_choice.v                                                      *)
(* auteur: alex@sysal.ibp.fr                                               *)
(* date: 19/10/95                                                          *)
(***************************************************************************)
Require Export applications.

(***************************************************************************)
(* Ennonce de l'axiome du choix                                            *)
(***************************************************************************)
Axiom
  axs_choice :
    forall (a I : E) (funa : fun_ a) (doma : dom a = I),
    (forall i : E, In i I -> App a funa i <> Vide) ->
    produit a I funa doma <> Vide.

(***************************************************************************)
(*                          Next : ZFrelations.v                           *)
(***************************************************************************)