diff --git a/FEM/Algebra/Finite_dim.v b/FEM/Algebra/Finite_dim.v
index f43007bef0a0fafc268e75f1922a8c0665308113..bd03d4bd98b4808c4ea61c09c01865673e0a3106 100644
--- a/FEM/Algebra/Finite_dim.v
+++ b/FEM/Algebra/Finite_dim.v
@@ -2858,6 +2858,27 @@ Proof. apply lmS_bijS_sub_dim_equiv; easy. Qed.
 End Linear_mapping_R_Facts3.
 
 
+Section Swap_fun_R.
+
+Context {E F : ModuleSpace R_Ring}.
+
+Context {n : nat}.
+Context {f : E -> 'R^n}.
+Hypothesis Hf : is_linear_mapping f.
+
+Variable PE : E -> Prop.
+
+Lemma is_free_scatter : surjS PE fullset f -> is_free (scatter f).
+Proof.
+move=> Hf1 L /fun_ext_rev HL; apply extF; intros i.
+rewrite -comb_lin_kronecker_in_r (comb_lin_scalF_compat _ _ _ _ (scalF_comm_R _ _)).
+destruct (Hf1 (kronecker i)) as [x [Hx <-]]; [easy |].
+rewrite zeroF -(fct_zero_eq x) -HL fct_comb_lin_r_eq; easy.
+Qed.
+
+End Swap_fun_R.
+
+
 Section Dual_family.
 
 Context {E : ModuleSpace R_Ring}.
diff --git a/FEM/FE.v b/FEM/FE.v
index fa4a599ca0bc646d2eec531e1999ebc8279d9084..da3e45ded28f8e822373440a66889c1150c7a3b8 100644
--- a/FEM/FE.v
+++ b/FEM/FE.v
@@ -40,42 +40,6 @@ From FEM Require Import Compl Algebra geometry poly_Lagrange P_approx_k  binomia
 
 Local Open Scope R_scope.
 
-Section bijS_Defs.
-
-Variable d : nat. (* dimension de l'espace *)
-Variable n : nat. (* n = dimension de P = cardinal of Sigma *)
-
-Variable P : FRd d -> Prop.
-
-(* Il existe une base B de P de taille n -> P sev de F dim n *)
-Hypothesis P_has_dim : has_dim P n.
-
-Let PC := has_dim_compatible_ms P_has_dim.
-
-Local Coercion Pval (p : sub_ms PC) : FRd d := val p.
-
-(* TODO FC 19/02/24 : generaliser et deplacer dans Sub_struct.v *)
-Lemma bijS_is_free : forall sigma : FRd d-> 'R^n,
-  is_linear_mapping sigma ->
-    bijS P fullset sigma -> is_free (scatter sigma).
-Proof.
-intros sigma Hs1 Hs2.
-apply bijS_ex_uniq in Hs2.
-destruct Hs2 as (Hs2,Hs3).
-intros L HL.
-apply extF; intros k.
-rewrite <- comb_lin_kronecker_in_r.
-apply trans_eq with (comb_lin L (fun j => kronecker k j)).
-apply comb_lin_scalF_compat, scalF_comm_R.
-specialize (Hs3 (kronecker k)) as (pk,((Hpk1,Hpk2),_)); try easy.
-rewrite <- Hpk2.
-apply trans_eq with (comb_lin L (scatter sigma) pk).
-2: rewrite HL; easy.
-rewrite fct_comb_lin_r_eq; easy.
-Qed.
-
-End bijS_Defs.
-
 Section FE_Local_simplex.
 
 Inductive shape_type :=  Simplex  | Quad.
@@ -214,15 +178,9 @@ Proof.
 apply is_free_is_basis.
 apply fe.
 intros i; apply shape_fun_correct.
-eapply is_dual_is_free_rev.
-intros i; apply Sigma_lin_map.
+apply (is_dual_is_free_rev _ _ (Sigma_lin_map fe)).
 intros i j; apply shape_fun_correct.
-apply bijS_is_free with (P := P_approx fe).
-simpl.
-2: apply (unisolvence fe).
-destruct fe; simpl.
-rewrite gather_is_linear_mapping_compat in Sigma_lin_map0.
-easy.
+apply (is_free_scatter (P_approx fe)), bijS_surjS, (unisolvence fe).
 Qed.
 
 (* From Aide-memoire EF Alexandre Ern : Definition 4.4 p. 78 *)