diff --git a/FEM/Finite_dim.v b/FEM/Finite_dim.v
index 358cf7d8af67439e2440f0a7a5c3d00941527822..0c89fe8e7c0d53246823b55bcd0a86fb978f78cb 100644
--- a/FEM/Finite_dim.v
+++ b/FEM/Finite_dim.v
@@ -21,6 +21,7 @@ apply compatible_g_is_linear_mapping.
 intros f l Hf. apply is_linear_mapping_f_scal; easy.
 Qed.
 
+(* sev -> ev *)
 Definition Lm := Sg_ModuleSpace compatible_linear_mapping.
 
 About val.
@@ -100,19 +101,52 @@ split.
 rewrite scal_zero_r.
 Admitted.*)
 
+Section Foo1.
+
+Context {E F : ModuleSpace R_Ring}.
+
+Variable dimPE : nat.
+Variable dimPF : nat.
+
+Variable PE : E -> Prop.
+Variable PF : F -> Prop.
+
+Hypothesis HE : compatible_finite PE dimPE.
+Hypothesis HF : compatible_finite PF dimPF.
+
+(* PE et PF sont des sev de E et F respectivement *)
+Let PE_compatible :=  compatible_finite_compatible_m PE dimPE HE.
+Let PF_compatible :=  compatible_finite_compatible_m PF dimPF HF.
+
+Local Definition UE := @Sg_ModuleSpace E PE PE_compatible.
+Local Definition UF := @Sg_ModuleSpace F PF PF_compatible.
+
+(*
+Lemma thm_rang :
+  forall (dimKer dimIm : nat),
+  forall f : UE -> UF, is_linear_mapping f ->
+  compatible_finite (image f E) dimIm ->
+  (*compatible_finite (Ker f) dimKer->*)
+  dimPE = dimIm + dimKer.
+Proof.
+Admitted.*)
+
+End Foo1.
+
+
 Section homogeneous_Cartesian_product.
 
 Context {E : ModuleSpace R_Ring}.
 Variable n : nat.
 
 Definition En_plus (f:'I_n -> E) (g:'I_n -> E) : ('I_n -> E) :=
-  fun x => plus (f x) (g x).
+  fun i => plus (f i) (g i).
 
 Definition En_scal (l:R) (f:'I_n -> E) : ('I_n -> E) :=
-  fun x => scal l (f x).
+  fun i => scal l (f i).
 
 Definition En_opp (f:'I_n -> E) : ('I_n -> E) :=
-  fun x => opp (f x).
+  fun i => opp (f i).
 
 Definition En_zero:'I_n -> E := fun _ => zero.
 
@@ -120,7 +154,7 @@ Lemma En_plus_comm: forall (f g:'I_n -> E), En_plus f g = En_plus g f.
 Proof.
 intros f g.
 apply functional_extensionality.
-intros x; apply plus_comm.
+intros i; apply plus_comm.
 Qed.
 
 Lemma En_plus_assoc:
@@ -128,21 +162,21 @@ Lemma En_plus_assoc:
 Proof.
 intros f g h.
 apply functional_extensionality.
-intros x; apply plus_assoc.
+intros i; apply plus_assoc.
 Qed.
 
 Lemma En_plus_zero_r: forall f:'I_n -> E, En_plus f En_zero = f.
 Proof.
 intros f.
 apply functional_extensionality.
-intros x; apply plus_zero_r.
+intros i; apply plus_zero_r.
 Qed.
 
 Lemma En_plus_opp_r: forall f:'I_n -> E, En_plus f (En_opp f) = En_zero.
 Proof.
 intros f.
 apply functional_extensionality.
-intros x; apply plus_opp_r.
+intros i; apply plus_opp_r.
 Qed.
 
 Definition En_AbelianGroup_mixin :=
@@ -164,7 +198,7 @@ Lemma En_scal_one: forall (u:'I_n -> E), En_scal one u = u.
 Proof.
 intros u.
 apply functional_extensionality.
-intros x; apply scal_one.
+intros i; apply scal_one.
 Qed.
 
 Lemma En_scal_distr_l: forall x (u v:'I_n -> E), En_scal x (plus u v) = En_plus (En_scal x u) (En_scal x v).
diff --git a/FEM/bijective.v b/FEM/bijective.v
new file mode 100644
index 0000000000000000000000000000000000000000..ef013fdb8e6aba6260369db4d96062ba9a98b342
--- /dev/null
+++ b/FEM/bijective.v
@@ -0,0 +1,237 @@
+From Coq Require Import FunctionalExtensionality ClassicalDescription ClassicalChoice ClassicalEpsilon.
+From Coq Require Import  Morphisms.
+From Coq Require Import Arith Lia Reals Lra.
+
+Add LoadPath "../Lebesgue" as Lebesgue.
+From Lebesgue Require Import Function.
+
+Add LoadPath "../LM" as LM.
+From LM Require Import linear_map.
+
+Section Funbij0.
+
+Context {E F : Type}.
+
+Variable PE : E -> Prop.
+Variable PF : F -> Prop.
+
+Variable f : E -> F.
+
+Definition is_inj : Prop :=
+  forall x y, PE x -> PE y -> f x = f y -> x = y.
+
+Definition is_surj : Prop :=
+  forall y, PF y -> exists x, PE x /\ f x = y.
+
+End Funbij0.
+
+Section Funbij1.
+
+Context {E F : Type}.
+
+Variable PE : E -> Prop.
+Variable PF : F -> Prop.
+
+Variable f : E -> F.
+Variable g : F -> E.
+
+Definition range : Prop :=
+  forall x, PE x -> PF (f x).
+
+Definition identity : Prop :=
+  forall x, PE x -> g (f x) = x.
+
+End Funbij1.
+
+Section Funbij2.
+
+Context {E F : Type}.
+
+Variable PE : E -> Prop.
+Variable PF : F -> Prop.
+
+Variable f : E -> F.
+Variable g : F -> E.
+
+Definition is_bij_id : Prop :=
+  range PE PF f /\ range PF PE g /\
+  identity PE f g /\ identity PF g f.
+
+Definition is_bij : Prop :=
+  forall y, PF y -> exists! x, PE x /\ f x = y.
+
+Lemma is_bij_id_is_bij : 
+  is_bij_id  <-> is_bij.
+Proof.
+split.
+(* <= *)
+intros [H1 [H2 [H3 H4]]].
+unfold is_bij; intros y Hy.
+exists (g y); repeat split.
+apply H2; easy.
+apply H4; easy.
+intros x' Hx'; destruct Hx' as [Y1 Y2].
+rewrite <- Y2.
+apply H3; easy.
+(* => *)
+intros H.
+unfold is_bij in H.
+unfold is_bij_id.
+repeat split.
+
+(*destruct (choice _ H).*)
+
+Admitted.
+
+End Funbij2.
+
+Section Funbij3.
+
+Context {E F : Type}.
+
+Variable PE : E -> Prop.
+Variable PF : F -> Prop.
+
+Variable f : E -> F.
+Variable g : F -> E.
+
+Lemma is_bij_id_equiv :
+  is_bij_id PE PF f g -> is_bij_id PF PE g f.
+Proof.
+now intros [H H'].
+Qed.
+
+Lemma is_bij_equiv : (* faux ! *)
+  is_bij PE PF f -> is_bij PF PE g.
+Proof.
+intros H x Hx.
+exists (f x); repeat split.
+unfold is_bij in H.
+Admitted.
+
+Lemma is_bij_id_is_surj :
+  is_bij_id PE PF f g -> is_surj PE PF f.
+Proof.
+intros [_ [H1 [_ H2]]] y Hy.
+exists (g y); split.
+now apply H1. 
+now apply H2.
+Qed.
+
+Lemma is_bij_id_is_inj :
+  is_bij_id PE PF f g -> is_inj PE f.
+Proof.
+intros [_ [_ [H _]]] x y1 Hx Hy1 H1.
+rewrite <- (H x), <- (H y1); try easy.
+now f_equiv.
+Qed.
+
+Lemma is_inj_is_surj_is_bij_id : 
+  is_inj PE f -> is_surj PE PF f -> is_bij PE PF f.
+Proof.
+intros H1 H2.
+unfold is_inj in H1.
+unfold is_surj in H2.
+unfold is_bij.
+intros y Hy.
+destruct (H2 y) as [x [H3 H4]]; try easy.
+exists x.
+repeat split; try easy.
+intros x1 Y.
+destruct Y as [Y1 Y2].
+erewrite H1; try easy.
+rewrite H4.
+rewrite Y2; easy.
+Qed.
+
+(*Definition comp_fun : E -> E := fun x => g (f x).*)
+
+(* fog bij alors f surj et g inj *)
+Lemma is_bij1 : 
+  is_bij PE PE (compose g f) -> is_surj PE PF f /\ is_inj PF g.
+Proof.
+intros H; split.
+unfold compose in H.
+apply is_bij_id_is_surj.
+apply is_bij_id_is_bij.
+admit.
+Admitted.
+
+(* Si f et g bij alors f o g est aussi bijective. *)
+Lemma is_bij2 :
+  is_bij PE PF f -> is_bij PF PE g -> is_bij PF PF (compose f g).
+Proof.
+intros H1 H2.
+Admitted.
+
+End Funbij3.
+
+Section Funbij4.
+
+Context {E F G: Type}.
+
+Variable PE : E -> Prop.
+Variable PF : F -> Prop.
+Variable PG : G -> Prop.
+
+Variable f : E -> F.
+Variable g : F -> G.
+
+(* f et g inj alors gof est inj *)
+Lemma is_bij3 :
+  is_inj PE f -> is_inj PF g -> is_inj PE (compose g f).
+Proof.
+Admitted.
+
+(* gof inj alors f est inj *)
+Lemma is_bij4 :
+  is_inj PE (compose g f) -> is_inj PE f.
+Proof.
+Admitted.
+
+(* f bij alors f-1 bij et (f-1)-1 = f *)
+(*Lemma is_bij4 : 
+  is_bij PE PF f -> 
+    is_bij PF PE (fun x => preimage f PF x) /\
+    preimage (preimage f PF) PE = image f PE.
+Proof.
+Admitted.*)
+
+(* f et g bij alors gof bij et (gof)^{-1} = f^{-1} o g^{-1}*)
+(* TODO: utiliser le lemme preimage_compose *)
+Lemma is_bij6 : 
+  is_bij PE PF f -> is_bij PF PG g -> 
+    is_bij PE PG (compose g f) /\ 
+  preimage (compose g f) PG = preimage f (preimage g PG).
+Proof.
+Admitted.
+
+End Funbij4.
+
+Section Fun_ker.
+Context {E F : ModuleSpace R_Ring}.
+
+Variable PE : E -> Prop.
+Variable PF : F -> Prop.
+
+Variable f : E -> F.
+
+Hypothesis Hf : is_linear_mapping f.
+
+Definition kerf : E -> Prop := fun x => 
+  f x = zero.
+
+(*
+Lemma is_inj_ker : 
+  is_inj PE f <-> forall x, kerf x = zero.
+Proof.
+Admitted.
+
+Lemma is_surj_image : 
+  is_surj PE f <-> image f PE = F.
+Proof.
+Admitted.
+*)
+
+End Fun_ker.
+
diff --git a/FEM/finite_element_1.v b/FEM/finite_element_1.v
index 94c76db26822d7715f5ea4ab592c44e6efc4ec1b..b7442fecaf9b5cd457f8163584cf4aea53746b17 100644
--- a/FEM/finite_element_1.v
+++ b/FEM/finite_element_1.v
@@ -60,7 +60,11 @@ Hypothesis P_compatible_finite : compatible_finite P n.
 (* Il existe une base B de P de taille n -> P sev de F dim n *)
 Let P_compatible :=  compatible_finite_compatible_m P n P_compatible_finite.
 
-(* Pol is a Set of elements that verify the property P *)
+Search bijective.
+(* P sev de dimension n de F -> P est un MS *)
+(* TODO: Choice to make:
+     - Pol est un espace de polynôme de Mathcomp car on ne sait rien sur P.
+     - Pol est un espace vectoriel de fonctions de dim finie *)
 Definition Pol := Sg_ModuleSpace (P_compatible).
 
 (* FC: quelle est l'utilité de cette définition ?
@@ -130,11 +134,9 @@ Record FE : Type := mk_FE {
   Rd := 'I_d -> R ; (* is R^d ;  was vectType R  ;*) 
   ndof : nat ; (* nb of degrees of freedom - eg number of nodes for Lagrange. *)
   nvtx : nat ; (* number of vertices *)
-
   d_pos :    (0 < d)%nat ;
   ndof_pos : (0 < ndof)%nat ;
   nvtx_pos : (0 < nvtx)%nat ;
-
   vtx : 'I_nvtx -> ('I_d -> R) (* -> E R_MS *) ; (* vertices of geometrical element *)
   K_geom : ('I_d -> R) -> Prop := convex_envelop nvtx vtx (*TODO *) ;
                         (* geometrical element *)
diff --git a/Lebesgue/Function.v b/Lebesgue/Function.v
index d2f53cff95f06dad8c5dc7163970607e02f19cb5..3084cf53cf3725864c7907acbf04fc7960238916 100644
--- a/Lebesgue/Function.v
+++ b/Lebesgue/Function.v
@@ -47,8 +47,8 @@ Definition preimage : U1 -> Prop := fun x1 => A2 (f x1).
 
 Context {U3 : Type}. (* Universe. *)
 
-Variable f23 : U2 -> U3. (* Function. *)
 Variable f12 : U1 -> U2. (* Function. *)
+Variable f23 : U2 -> U3. (* Function. *)
 
 Definition compose : U1 -> U3 := fun x1 => f23 (f12 x1).