Function_sub:

Add and prove RgS_comp.

FEM/Compl/Function_sub.v

@@ -217,9 +217,11 @@ Lemma preimage_RgS_preimage :
   preimage f (RgS (preimage f PF) f) = preimage f PF.
 Proof. apply preimage_of_image_of_preimage. Qed.
 
-(* TODO FC (04/12/2023): state and prove this.
-Lemma RgS_comp : RgS PE (g \o f) = 
-*)
+Lemma RgS_comp : RgS PE (g \o f) = RgS (RgS PE f) g.
+Proof.
+apply subset_ext_equiv; split; intros z;
+    [intros [x Hx] | intros [y [x Hx]]; fold ((g \o f) x)]; easy.
+Qed.
 
 Lemma funS_full_l :
   forall PF (f : E -> F), incl (Rg f) PF -> funS fullset PF f.