proposition: Lemma component_equality_to_product t (A A': op_type carrier t) (B B': ∀ i, op_type (carriers i) t): (∀ i, B i = B' i) → nqe A B → nqe A' B' → A = A'.
proof: Proof. Proof with auto. induction t; simpl in *; intros BE ABE ABE'. intro. rewrite ABE, ABE'... intros x y U. apply (IHt (A x) (A' y) (λ i, B i (x i)) (λ i, B' i (y i)))... intros. apply BE, U. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories MathClasses.categories.varieties