diff --git a/FEM/Algebra/Finite_dim.v b/FEM/Algebra/Finite_dim.v
index f11683fd5e1a00c7ec235d14bf7cde1fff6904b6..15c52188f99e7fbb258b53bb7a34cf7341e8cd82 100644
--- a/FEM/Algebra/Finite_dim.v
+++ b/FEM/Algebra/Finite_dim.v
@@ -2762,7 +2762,7 @@ Proof. rewrite RgS_gen_eq//; apply (RgS_is_finite_dim HPE Hf). Qed.
 Lemma lmS_surjS_gen_dim_equiv :
   surjS PE PF f <-> has_dim (RgS_gen PE PF f) nPF.
 Proof.
-rewrite surjS_equiv RgS_gen_eq//; split.
+rewrite surjS_RgS_gen_equiv RgS_gen_eq//; split.
 intros; subst; easy.
 intros Hf2; apply (has_dim_eq Hf1 Hf2 HPF); easy.
 Qed.
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 3d9924310763c7c6a59643e14209cc662c4f4239..702bb6d6c64c25b79ce44764287f7994254ef52e 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -4984,8 +4984,7 @@ apply extF; intros i2; destruct (im_dec f i2) as [[i1 <-] | Hi2].
 apply maskPF_correct_l; easy.
 rewrite -incl_compl_equiv in HA2; specialize (HA2 i2);
     unfold compl, neqF in HA2; rewrite NNPP_equiv in HA2.
-rewrite HA2; [ apply maskPF_correct_r; rewrite -Rg_compl_equiv |];
-    rewrite Rg_compl; easy.
+rewrite HA2; [ apply maskPF_correct_r |]; rewrite Rg_compl; easy.
 Qed.
 
 Lemma filterPF_unfunF :
diff --git a/FEM/Algebra/MonoidComp.v b/FEM/Algebra/MonoidComp.v
index 4338050dc7f9727f260566edb412f8b1659f67b7..548295d2c45eccd59330e25557edf5c0a457ca11 100644
--- a/FEM/Algebra/MonoidComp.v
+++ b/FEM/Algebra/MonoidComp.v
@@ -217,7 +217,7 @@ Lemma comp_n_funS :
 Proof.
 intros n f Hf; induction n as [|n Hn];
     [rewrite comp_n_nil; [apply funS_id | easy] | rewrite comp_n_ind_l].
-apply funS_comp_compat with PE; [apply Hn; unfold liftF_S |]; easy.
+apply (funS_comp_compat PE); [apply Hn; unfold liftF_S |]; easy.
 Qed.
 
 Context {n : nat}.
@@ -295,7 +295,7 @@ intros n f j Hf; induction n as [|n Hn];
     [rewrite comp_n_part_nil; [apply funS_id | easy] |].
 destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
     [rewrite (comp_n_part_0 _ _ Hj0); apply funS_id |].
-rewrite comp_n_part_ind_l; apply funS_comp_compat with PE; [apply Hn |].
+rewrite comp_n_part_ind_l; apply (funS_comp_compat PE); [apply Hn |].
 intros; apply (widenF_liftF_S_P_compat _ Hj0 Hf); easy.
 apply (widenF_0_P_compat Hj0 Hf).
 Qed.
diff --git a/FEM/Algebra/Sub_struct.v b/FEM/Algebra/Sub_struct.v
index 144e8768a5b12cf814afde1bbd733fbe7f7f575f..5c5ecc3d8d2b1f44bc26d6388081add2d7828f63 100644
--- a/FEM/Algebra/Sub_struct.v
+++ b/FEM/Algebra/Sub_struct.v
@@ -3289,7 +3289,7 @@ Qed.
 
 Lemma surjS_gen_aff_lin_equiv_alt : surjS PE PF f <-> incl PW (RgS PV lf).
 Proof.
-rewrite surjS_gen_aff_lin_equiv -RgS_gen_full_equiv; apply surjS_equiv.
+rewrite surjS_gen_aff_lin_equiv -RgS_gen_full_equiv; apply surjS_RgS_gen_equiv.
 Qed.
 
 Lemma bijS_gen_aff_lin_equiv : bijS PE PF f <-> bijS PV PW lf.
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index 0939070fb3be712313b5919721d912aa188a93ad..68ff8e0025b1278e9b627459d079482da68fe996 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -58,7 +58,7 @@ From FEM Require Import logic_compl.
   'f_inv Hf' is the inverse of any function from any proof 'Hf' of its bijectivity.
   The inverse of any bijective function is unique and bijective.
   Involutive functions are the bijective functions equal to their inverse.
- *)
+*)
 
 
 Section Functional_extensionality_Facts.
@@ -231,14 +231,6 @@ Proof. intros; split; [intros [x1 _]; exists x1 | move=> [x1 <-]]; easy. Qed.
 Lemma Rg_compl : forall {x2}, ~ Rg f x2 <-> forall x1, f x1 <> x2.
 Proof. intros; rewrite -iff_not_r_equiv not_all_not_ex_equiv; apply Rg_ex. Qed.
 
-Lemma Rg_equiv : forall {x2}, Rg f x2 <-> image f fullset x2.
-Proof.
-intros; rewrite Rg_ex image_eq; split; intros [x1 Hx1]; exists x1; easy.
-Qed.
-
-Lemma Rg_compl_equiv : forall {x2}, ~ Rg f x2 <-> ~ image f fullset x2.
-Proof. intros; rewrite -iff_not_equiv; apply Rg_equiv. Qed.
-
 Lemma Rg_full_equiv : Rg f = fullset <-> incl fullset (Rg f).
 Proof. split; intros Hf; [rewrite Hf | apply subset_ext_equiv]; easy. Qed.
 
diff --git a/FEM/Compl/Function_sub.v b/FEM/Compl/Function_sub.v
index 414a232eceb8c1421a42883cfe935cbcd57c2255..10b0ee9af3bddad1664dda39f887715a3dcbb425 100644
--- a/FEM/Compl/Function_sub.v
+++ b/FEM/Compl/Function_sub.v
@@ -28,6 +28,7 @@ From FEM Require Import logic_compl Function_compl.
   Let 'f : T1 -> T2' for any types 'T1' and 'T2'.
   Let 'P1' and 'P2' respectively be subsets of 'T1' and 'T2'.
 
+  'same_funS P1 f g' states that 'f' and 'g' are equal on 'P1'.
   'RgS P1 f' is the range of 'f' restricted to 'P1' (an alias for 'image f P1').
   'funS P1 P2 f' states that 'f' is a total function from 'P1' to 'P2',
     namely that 'RgS P1 f' is included in 'P2'.
@@ -39,8 +40,7 @@ From FEM Require Import logic_compl Function_compl.
     (definition similar to cancel).
   'bijS P1 P2 f' states that 'f' is bijective from 'P1' onto 'P2'
     (definition similar to bijective).
-
- *)
+*)
 
 
 Section Fun_sub_Def1.
@@ -52,13 +52,15 @@ Variable P2 : T2 -> Prop.
 
 Variable f : T1 -> T2.
 
+Definition same_funS (g : T1 -> T2) : Prop := forall x1, P1 x1 -> f x1 = g x1.
+
 Definition RgS : T2 -> Prop := image f P1.
 Definition RgS_gen : T2 -> Prop := inter P2 RgS.
 
 Definition funS : Prop := incl RgS P2.
 
 Definition injS : Prop :=
-  forall x1 x2, P1 x1 -> P1 x2 -> f x1 = f x2 -> x1 = x2.
+  forall x1 y1, P1 x1 -> P1 y1 -> f x1 = f y1 -> x1 = y1.
 
 Definition surjS : Prop := forall x2, P2 x2 -> exists x1, P1 x1 /\ f x1 = x2.
 
@@ -91,6 +93,27 @@ Qed.
 End Fun_sub_Def2.
 
 
+Section Same_funS_Facts.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+
+Lemma same_funS_refl : forall (f : T1 -> T2), same_funS P1 f f.
+Proof. easy. Qed.
+
+Lemma same_funS_sym :
+  forall {f g : T1 -> T2}, same_funS P1 f g -> same_funS P1 g f.
+Proof. move=>> H x1 Hx1; rewrite H; easy. Qed.
+
+Lemma same_funS_trans :
+  forall g {f h : T1 -> T2},
+    same_funS P1 f g -> same_funS P1 g h -> same_funS P1 f h.
+Proof. move=>> H1 H2 x1 Hx1; rewrite H1// H2; easy. Qed.
+
+End Same_funS_Facts.
+
+
 Section RgS_Facts1.
 
 Context {T1 T2 : Type}.
@@ -128,11 +151,32 @@ End RgS_Facts1.
 
 Section RgS_Facts2.
 
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+
+Lemma RgS_ext : forall g, same_funS P1 f g -> RgS P1 f = RgS P1 g.
+Proof.
+intros g Hg; apply subset_ext_equiv; split; intros x2; rewrite !RgS_ex;
+    intros [x1 Hx1]; exists x1; [rewrite -Hg | rewrite Hg]; easy.
+Qed.
+
+Lemma RgS_gen_ext :
+  forall g, same_funS P1 f g -> RgS_gen P1 P2 f = RgS_gen P1 P2 g.
+Proof. unfold RgS_gen; move=> g /(RgS_ext g) ->; easy. Qed.
+
+End RgS_Facts2.
+
+
+Section RgS_Facts3.
+
 Context {T1 T2 T3 : Type}.
 
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
-Context {P3 : T3 -> Prop}.
 
 Context {f : T1 -> T2}.
 Context {g : T2 -> T3}.
@@ -185,7 +229,7 @@ Qed.
 Lemma Rg_comp_alt : Rg (g \o f) = RgS (Rg f) g.
 Proof. apply Rg_comp. Qed.
 
-End RgS_Facts2.
+End RgS_Facts3.
 
 
 Section FunS_Facts1.
@@ -216,75 +260,101 @@ Context {T1 T2 : Type}.
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
 
-Lemma funS_id : funS P1 P1 id.
-Proof. apply funS_equiv; easy. Qed.
+Variable f : T1 -> T2.
+Context {g : T1 -> T2}.
+
+Lemma funS_ext : same_funS P1 f g -> funS P1 P2 f -> funS P1 P2 g.
+Proof. move=> Hg Hf x2; rewrite -(RgS_ext _ Hg); auto. Qed.
 
 End FunS_Facts2.
 
 
 Section FunS_Facts3.
 
+Context {T : Type}.
+
+Variable P : T -> Prop.
+
+Lemma funS_id : funS P P id.
+Proof. apply funS_equiv; easy. Qed.
+
+End FunS_Facts3.
+
+
+Section FunS_Facts4.
+
 Context {T1 T2 : Type}.
 
-Context {P1 : T1 -> Prop}.
+Variable P1 : T1 -> Prop.
 Context {P2 : T2 -> Prop}.
 
-Context {f : T1 -> T2}.
+Variable f : T1 -> T2.
 
-Lemma funS_full_l :
-  forall P2 (f : T1 -> T2), incl (Rg f) P2 -> funS fullset P2 f.
+Lemma funS_full_l : forall {f : T1 -> T2}, incl (Rg f) P2 -> funS fullset P2 f.
 Proof. easy. Qed.
 
-Lemma funS_full_r : forall P1 (f : T1 -> T2), funS P1 fullset f.
+Lemma funS_full_r : funS P1 fullset f.
 Proof. easy. Qed.
 
-Lemma funS_full : forall (f : T1 -> T2), funS fullset fullset f.
+Lemma funS_full : funS fullset fullset f.
 Proof. easy. Qed.
 
-End FunS_Facts3.
+End FunS_Facts4.
 
 
-Section FunS_Facts4.
+Section FunS_Facts5.
 
 Context {T1 T2 T3 : Type}.
 
-Variable P1 : T1 -> Prop.
+Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
-Variable P3 : T3 -> Prop.
+Context {P3 : T3 -> Prop}.
 
-Variable f : T1 -> T2.
-Variable g : T2 -> T3.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T3}.
 
 Lemma funS_comp_compat : funS P1 P2 f -> funS P2 P3 g -> funS P1 P3 (g \o f).
-Proof.
-move=> /funS_equiv Hf /funS_equiv Hg _ [x1 Hx1]; apply Hg, Hf; easy.
-Qed.
+Proof. rewrite !funS_equiv; intros Hf Hg x1 Hx1; apply Hg; auto. Qed.
 
-End FunS_Facts4.
+End FunS_Facts5.
 
 
 Section InjS_Facts1.
 
 Context {T1 T2 : Type}.
 
+Context {P1 : T1 -> Prop}.
+
 Variable f : T1 -> T2.
+Context {g : T1 -> T2}.
 
-Lemma inj_S_equiv : injective f <-> injS fullset f.
-Proof. split; intros Hf; move=>>; [auto | apply Hf; easy]. Qed.
+Lemma injS_ext : same_funS P1 f g -> injS P1 f -> injS P1 g.
+Proof. intros Hg Hf x1 y1 Hx1 Hy1; rewrite -!Hg; auto. Qed.
 
 End InjS_Facts1.
 
 
 Section InjS_Facts2.
 
+Context {T1 T2 : Type}.
+
+Context {f : T1 -> T2}.
+
+Lemma inj_S_equiv : injective f <-> injS fullset f.
+Proof. split; intros Hf; move=>>; [auto | apply Hf; easy]. Qed.
+
+End InjS_Facts2.
+
+
+Section InjS_Facts3.
+
 Context {T1 T2 T3 : Type}.
 
-Variable P1 : T1 -> Prop.
+Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
-Variable P3 : T3 -> Prop.
 
-Variable f : T1 -> T2.
-Variable g : T2 -> T3.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T3}.
 
 Lemma injS_comp_compat :
   funS P1 P2 f -> injS P1 f -> injS P2 g -> injS P1 (g \o f).
@@ -292,12 +362,24 @@ Proof.
 intros Hf0 Hf Hg x1 y1 Hx1 Hy1 H1; apply Hf, Hg; try apply Hf0; easy.
 Qed.
 
+End InjS_Facts3.
+
+
+Section InjS_Facts4.
+
+Context {T1 T2 T3 : Type}.
+
+Context {P1 : T1 -> Prop}.
+
+Context {f : T1 -> T2}.
+Variable g : T2 -> T3.
+
 Lemma injS_comp_reg : injS P1 (g \o f) -> injS P1 f.
 Proof.
 intros H x1 y1 Hx1 Hy1 H1; apply H; try rewrite comp_correct H1; easy.
 Qed.
 
-End InjS_Facts2.
+End InjS_Facts4.
 
 
 Section SurjS_Facts1.
@@ -310,9 +392,7 @@ Context {P2 : T2 -> Prop}.
 Context {f : T1 -> T2}.
 
 Lemma surjS_correct : incl P2 (RgS P1 f) -> surjS P1 P2 f.
-Proof.
-intros Hf x2 Hx2; destruct (Hf x2 Hx2) as [x1 Hx1]; exists x1; easy.
-Qed.
+Proof. intros H x2 Hx2; destruct (H x2 Hx2) as [x1 Hx1]; exists x1; easy. Qed.
 
 Lemma surjS_rev : surjS P1 P2 f -> RgS_gen P1 P2 f = P2.
 Proof.
@@ -320,6 +400,34 @@ intros Hf; apply incl_antisym; intros x2 Hx2; [apply Hx2 |].
 destruct (Hf _ Hx2) as [x1 Hx1]; apply (RgS_gen_correct x1); easy.
 Qed.
 
+End SurjS_Facts1.
+
+
+Section SurjS_Facts2.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Variable f : T1 -> T2.
+Context {g : T1 -> T2}.
+
+Lemma surjS_ext : same_funS P1 f g -> surjS P1 P2 f -> surjS P1 P2 g.
+Proof.
+intros Hg Hf x2 Hx2; destruct (Hf x2 Hx2) as [x1 Hx1];
+    exists x1; rewrite -Hg; easy.
+Qed.
+
+End SurjS_Facts2.
+
+
+Section SurjS_Facts3.
+
+Context {T1 T2 : Type}.
+
+Context {f : T1 -> T2}.
+
 Lemma surj_S_equiv : surjective f <-> surjS fullset fullset f.
 Proof.
 split; intros Hf.
@@ -327,10 +435,10 @@ intros x2 _; destruct (Hf x2) as [x1 Hx1]; exists x1; easy.
 intros x2; destruct (Hf x2) as [x1 Hx1]; [| exists x1]; easy.
 Qed.
 
-End SurjS_Facts1.
+End SurjS_Facts3.
 
 
-Section SurjS_Facts2.
+Section SurjS_Facts4.
 
 Context {T1 T2 : Type}.
 
@@ -339,31 +447,35 @@ Context {P2 : T2 -> Prop}.
 
 Context {f : T1 -> T2}.
 
-Lemma surjS_equiv : surjS P1 P2 f <-> RgS_gen P1 P2 f = P2.
+Lemma surjS_RgS_gen_equiv : surjS P1 P2 f <-> RgS_gen P1 P2 f = P2.
 Proof.
-split; [apply surjS_rev |].
-intros Hf; rewrite -Hf; apply surjS_correct, inter_lb_r.
+split; [apply surjS_rev | move=> <-; apply surjS_correct, inter_lb_r].
 Qed.
 
-Lemma surjS_equiv_alt : surjS P1 P2 f <-> incl P2 (RgS P1 f).
-Proof. rewrite surjS_equiv; apply RgS_gen_full_equiv. Qed.
+Lemma surjS_RgS_equiv_alt : surjS P1 P2 f <-> incl P2 (RgS P1 f).
+Proof. rewrite surjS_RgS_gen_equiv; apply RgS_gen_full_equiv. Qed.
+
+Lemma surjS_RgS_equiv : funS P1 P2 f -> surjS P1 P2 f <-> RgS P1 f = P2.
+Proof.
+intros Hf; rewrite -(RgS_gen_full_equiv_alt Hf); apply surjS_RgS_gen_equiv.
+Qed.
 
 Lemma surjS_RgS : forall P1 (f : T1 -> T2), surjS P1 (RgS P1 f) f.
 Proof. intros; apply surjS_correct; easy. Qed.
 
-End SurjS_Facts2.
+End SurjS_Facts4.
 
 
-Section SurjS_Facts3.
+Section SurjS_Facts5.
 
 Context {T1 T2 T3 : Type}.
 
-Variable P1 : T1 -> Prop.
+Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
-Variable P3 : T3 -> Prop.
+Context {P3 : T3 -> Prop}.
 
-Variable f : T1 -> T2.
-Variable g : T2 -> T3.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T3}.
 
 Lemma surjS_comp_compat :
   surjS P1 P2 f -> surjS P2 P3 g -> surjS P1 P3 (g \o f).
@@ -373,35 +485,140 @@ intros Hf Hg x3 Hx3;
 exists x1; split; [| rewrite comp_correct Hx1b]; easy.
 Qed.
 
+End SurjS_Facts5.
+
+
+Section SurjS_Facts6.
+
+Context {T1 T2 T3 : Type}.
+
+Variable P1 : T1 -> Prop.
+Context {P2 : T2 -> Prop}.
+Context {P3 : T3 -> Prop}.
+
+Variable f : T1 -> T2.
+Context {g : T2 -> T3}.
+
 Lemma surjS_comp_reg : funS P1 P2 f -> surjS P1 P3 (g \o f) -> surjS P2 P3 g.
 Proof.
 intros Hf H x3 Hx3; destruct (H _ Hx3) as [x1 [Hx1a Hx1b]].
 exists (f x1); split; [apply Hf |]; easy.
 Qed.
 
-End SurjS_Facts3.
+End SurjS_Facts6.
 
 
 Section CanS_Facts1.
 
-Context {T1 T2 T3 : Type}.
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f f' : T1 -> T2}.
+Context {g g' : T2 -> T1}.
+
+Lemma canS_ext_l : same_funS P1 f f' -> canS P1 f g -> canS P1 f' g.
+Proof. intros Hf H x1 Hx1; rewrite -Hf//; auto. Qed.
+
+Lemma canS_ext_r :
+  funS P1 P2 f -> same_funS P2 g g' -> canS P1 f g -> canS P1 f g'.
+Proof. intros Hf Hg H x1 Hx1; rewrite -Hg//; [apply H | apply Hf]; easy. Qed.
+
+End CanS_Facts1.
+
+
+Section CanS_Facts2.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f f' : T1 -> T2}.
+Context {g g' : T2 -> T1}.
+
+Lemma canS_ext :
+  funS P1 P2 f -> same_funS P1 f f' -> same_funS P2 g g' ->
+  canS P1 f g -> canS P1 f' g'.
+Proof. move=> H1 H2 H3 /(canS_ext_r H1 H3) /(canS_ext_l H2); easy. Qed.
+
+End CanS_Facts2.
+
+
+Section CanS_Facts3.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+
+Context {f : T1 -> T2}.
+Variable g : T2 -> T1.
+
+Lemma canS_injS : canS P1 f g -> injS P1 f.
+Proof. move=> H x1 y1 Hx1 Hy1 /(f_equal g); rewrite !H; easy. Qed.
+
+End CanS_Facts3.
+
+
+Section CanS_Facts4.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+Variable g : T2 -> T1.
+
+Lemma canS_surjS : funS P2 P1 g -> canS P2 g f -> surjS P1 P2 f.
+Proof.
+intros Hg H x2 Hx2; exists (g x2); split; [apply Hg | rewrite H]; easy.
+Qed.
+
+End CanS_Facts4.
+
+
+Section CanS_Facts5.
+
+Context {T1 T2 : Type}.
 
 Variable P1 : T1 -> Prop.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+Context {g : T2 -> T1}.
+
+Lemma injS_canS_sym :
+  funS P1 P2 f -> funS P2 P1 g -> injS P2 g -> canS P1 f g -> canS P2 g f.
+Proof.
+intros H1 H2 H3 H4 x2 Hx2;
+    apply H3; [apply H1, Im | easy | rewrite H4//]; apply H2; easy.
+Qed.
+
+End CanS_Facts5.
+
+
+Section CanS_Facts6.
+
+Context {T1 T2 T3 : Type}.
+
+Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
-Variable P3 : T3 -> Prop.
+Context {P3 : T3 -> Prop}.
 
-Variable f : T1 -> T2.
-Variable g : T2 -> T3.
+Context {f : T1 -> T2}.
+Context {f1 : T2 -> T1}.
+Context {g : T2 -> T3}.
+Context {g1 : T3 -> T2}.
 
 Lemma canS_comp_compat :
-  forall {f1 g1},
-    funS P1 P2 f -> canS P1 f f1 -> canS P2 g g1 ->
-    canS P1 (g \o f) (f1 \o g1).
+  funS P1 P2 f -> canS P1 f f1 -> canS P2 g g1 -> canS P1 (g \o f) (f1 \o g1).
 Proof.
-move=>> /funS_equiv H1 H2 H3 x1 Hx1; rewrite -> !comp_correct, H3, H2; auto.
+move=> /funS_equiv H1 H2 H3 x1 Hx1; rewrite -> !comp_correct, H3, H2; auto.
 Qed.
 
-End CanS_Facts1.
+End CanS_Facts6.
 
 
 Section BijS_Facts1.
@@ -412,6 +629,29 @@ Hypothesis HT1 : inhabited T1.
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
 
+Variable f : T1 -> T2.
+Context {g : T1 -> T2}.
+
+Lemma bijS_ext : same_funS P1 f g -> bijS P1 P2 f -> bijS P1 P2 g.
+Proof.
+move=> Hg /bijS_ex [f1 [Hf1 [Hf2 [Hf3 Hf4]]]];
+    apply bijS_ex; exists f1; repeat split; [| easy |..].
+apply (funS_ext f), Hf1; easy.
+apply (canS_ext_l Hg Hf3).
+apply (canS_ext_r Hf2 Hg Hf4).
+Qed.
+
+End BijS_Facts1.
+
+
+Section BijS_Facts2.
+
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
 Context {f : T1 -> T2}.
 
 Lemma bijS_ex_uniq :
@@ -448,19 +688,24 @@ Lemma bijS_ex_uniq_equiv :
   funS P1 P2 f /\ (forall x2, P2 x2 -> exists! x1, P1 x1 /\ f x1 = x2).
 Proof. split; [apply bijS_ex_uniq | intros; apply bijS_ex_uniq_rev; easy]. Qed.
 
-End BijS_Facts1.
+End BijS_Facts2.
 
 
-Section BijS_Facts2.
+Section BijS_Facts3.
 
 Context {T1 T2 : Type}.
-Hypothesis HT1 : inhabited T1.
 
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
 
 Context {f : T1 -> T2}.
 
+Lemma bijS_RgS : bijS P1 P2 f -> RgS P1 f = P2.
+Proof.
+intros [g [Hf [Hg [H1 H2]]]]; apply subset_ext_equiv; split; [easy |].
+intros x2 Hx2; rewrite -(H2 _ Hx2); apply Im, Hg; easy.
+Qed.
+
 Lemma bijS_funS : bijS P1 P2 f -> funS P1 P2 f.
 Proof. intros [g Hg]; apply Hg. Qed.
 
@@ -473,6 +718,19 @@ Qed.
 Lemma bijS_surjS : bijS P1 P2 f -> surjS P1 P2 f.
 Proof. move=> [g [_ [/funS_equiv Hg [_ Hf]]]] x2 Hx2; exists (g x2); auto. Qed.
 
+End BijS_Facts3.
+
+
+Section BijS_Facts4.
+
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+
 Lemma injS_surjS_bijS :
   funS P1 P2 f -> injS P1 f -> surjS P1 P2 f -> bijS P1 P2 f.
 Proof.
@@ -488,16 +746,15 @@ split; [apply (bijS_injS P2) | apply bijS_surjS]; easy.
 apply injS_surjS_bijS; easy.
 Qed.
 
-End BijS_Facts2.
+End BijS_Facts4.
 
 
-Section BijS_Facts3.
+Section BijS_Facts5.
 
 Context {T1 T2 : Type}.
 Hypothesis HT1 : inhabited T1.
 
 Context {P1 : T1 -> Prop}.
-Context {P2 : T2 -> Prop}.
 
 Context {f : T1 -> T2}.
 
@@ -510,30 +767,29 @@ Qed.
 Lemma bij_S_equiv : bijective f <-> bijS fullset fullset f.
 Proof. rewrite bij_equiv bijS_equiv// inj_S_equiv surj_S_equiv; easy. Qed.
 
-End BijS_Facts3.
+End BijS_Facts5.
 
 
-Section BijS_Facts4.
+Section BijS_Facts6.
 
 Context {T1 T2 T3 : Type}.
 Hypothesis HT1 : inhabited T1.
-Hypothesis HT2 : inhabited T2.
 
-Variable P1 : T1 -> Prop.
+Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
-Variable P3 : T3 -> Prop.
+Context {P3 : T3 -> Prop}.
 
-Variable f : T1 -> T2.
-Variable g : T2 -> T3.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T3}.
 
 Lemma bijS_spec_comp_compat :
-  forall f1 g1,
+  forall {f1 g1},
     bijS_spec P1 P2 f f1 -> bijS_spec P2 P3 g g1 ->
     bijS_spec P1 P3 (g \o f) (f1 \o g1).
 Proof.
 intros f1 g1 [Hf1 [Hf2 [Hf3 Hf4]]] [Hg1 [Hg2 [Hg3 Hg4]]]; repeat split.
-1,2: apply funS_comp_compat with P2; easy.
-1,2: apply canS_comp_compat with P2; easy.
+1,2: apply (funS_comp_compat P2); easy.
+1,2: apply (canS_comp_compat P2); easy.
 Qed.
 
 Lemma bijS_comp_compat : bijS P1 P2 f -> bijS P2 P3 g -> bijS P1 P3 (g \o f).
@@ -541,25 +797,115 @@ Proof.
 intros [f1 Hf] [g1 Hg]; exists (f1 \o g1); apply bijS_spec_comp_compat; easy.
 Qed.
 
+End BijS_Facts6.
+
+
+Section BijS_Facts7.
+
+Context {T1 T2 T3 : Type}.
+Hypothesis HT1 : inhabited T1.
+
+Context {P1 : T1 -> Prop}.
+Variable P2 : T2 -> Prop.
+Variable P3 : T3 -> Prop.
+
+Context {f : T1 -> T2}.
+Variable g : T2 -> T3.
+
 Lemma bijS_comp_injS : funS P1 P2 f -> bijS P1 P3 (g \o f) -> injS P1 f.
 Proof.
 intros H1 H2; move: (proj1 (bijS_equiv HT1) H2) => [_ [H3 _]].
 apply injS_comp_reg with g; easy.
 Qed.
 
-Lemma bijS_comp_surjS :
-  funS P1 P2 f -> bijS P1 P3 (g \o f) -> surjS P2 P3 g.
+End BijS_Facts7.
+
+
+Section BijS_Facts8.
+
+Context {T1 T2 T3 : Type}.
+Hypothesis HT1 : inhabited T1.
+
+Variable P1 : T1 -> Prop.
+Context {P2 : T2 -> Prop}.
+Context {P3 : T3 -> Prop}.
+
+Variable f : T1 -> T2.
+Context {g : T2 -> T3}.
+
+Lemma bijS_comp_surjS : funS P1 P2 f -> bijS P1 P3 (g \o f) -> surjS P2 P3 g.
 Proof.
 intros H1 H2; move: (proj1 (bijS_equiv HT1) H2) => [_ [_ H3]].
-apply surjS_comp_reg with P1 f; easy.
+apply (surjS_comp_reg P1 f); easy.
 Qed.
 
-End BijS_Facts4.
+End BijS_Facts8.
+
+
+Section BijS_Facts9.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+Context {g h : T2 -> T1}.
+
+Lemma bijS_canS_uniq_l :
+  bijS P1 P2 f -> funS P2 P1 g -> funS P2 P1 h ->
+  canS P2 g f -> canS P2 h f -> same_funS P2 g h.
+Proof.
+intros H1 H2 H3 H4 H5 x2 Hx2; apply (bijS_injS _ H1); [..| rewrite H5; auto];
+    [apply H2 | apply H3]; easy.
+Qed.
+
+Lemma bijS_canS_uniq_r :
+  bijS P1 P2 f -> canS P1 f g -> canS P1 f h -> same_funS P2 g h.
+Proof.
+move=> [f1 [_ [/funS_rev H1 [_ H2]]]] H3 H4 x2 Hx2; specialize (H1 _ Hx2).
+rewrite -(H2 _ Hx2) H3// H4; easy.
+Qed.
+
+End BijS_Facts9.
+
+
+Section BijS_Facts10.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+Context {g : T2 -> T1}.
+
+Lemma bijS_canS_sym : bijS P1 P2 f -> canS P1 f g <-> funS P2 P1 g /\ canS P2 g f.
+Proof.
+intros Hf; move: (proj1 (bijS_ex _ _ _) Hf) => [f1 [H1 [H2 [H3 H4]]]]; split.
+(* *)
+intros H5; split.
+apply: (funS_ext f1 _ H2); apply (bijS_canS_uniq_r Hf H3 H5).
+intros x2 Hx2; rewrite (bijS_canS_uniq_r Hf H5 H3); auto.
+(* *)
+intros [H5 H6] x1 Hx1; rewrite (bijS_canS_uniq_l Hf H5 H2 H6 H4);
+    [apply H3 | apply H1]; easy.
+Qed.
+
+Lemma bijS_canS_bijS : canS P1 f g -> bijS P1 P2 f -> bijS P2 P1 g.
+Proof.
+intros Hg Hf; apply bijS_ex; exists f; repeat split; [.. | easy].
+1,3: apply (bijS_canS_sym Hf), Hg.
+apply (bijS_funS Hf).
+Qed.
+
+End BijS_Facts10.
 
 
 Section F_invS_Def.
 
 Context {T1 T2 : Type}.
+
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.