proposition: Theorem isomorphic_first_isomorphism : A / cong_ker f ≅ B && in_image_hom f.
proof: Proof. exact (BuildIsomorphic def_first_isomorphism). Defined.
imports: HSet Colimits.Quotient Modalities.ReflectiveSubuniverse Classes.interfaces.canonical_names Classes.theory.ua_isomorphic Classes.theory.ua_subalgebra Classes.theory.ua_quotient_algebra