IsIsomorphism hom_third_isomorphism. Proof. unfold hom_third_isomorphism. destruct path_quotient_algebras_third_surjection. exact _. Qed.
Require Import Import algebra_notations quotient_algebra_notations isomorphic_notations.