diff --git a/FiniteSets/fsets/isomorphism.v b/FiniteSets/fsets/isomorphism.v
index 253b433..e72fa58 100644
--- a/FiniteSets/fsets/isomorphism.v
+++ b/FiniteSets/fsets/isomorphism.v
@@ -66,4 +66,9 @@ Section Iso.
     unfold Sect. apply repr_iso_id_r.
   Defined.
 
-End Iso.
\ No newline at end of file
+  Theorem fset_fsetc : FSet A = FSetC A.
+  Proof.
+    apply (equiv_path _ _)^-1.
+    exact repr_iso.
+  Defined.
+End Iso.