proposition: Lemma strong_binary_setoid_morphism_both_coordinates `{!StrongSetoid A} `{!StrongSetoid B} `{!StrongSetoid C} {f : A → B → C} `{∀ z, StrongSetoid_Morphism (f z)} `{∀ z, StrongSetoid_Morphism (λ x, f x z)} : StrongSetoid_BinaryMorphism f.
proof: Proof. split; try apply _. intros x₁ y₁ x₂ y₂ E. destruct (cotransitive E (f x₂ y₁)). left. now apply (strong_extensionality (λ x, f x y₁)). right. now apply (strong_extensionality (f x₂)). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.jections