Definition 2.1.1.7. Let
X1,
X2,
X3,
Y1,
Y2,
Y3 be sets,
φ1 : X1 ↔ Y1,
φ2 : X2 ↔ Y2,
φ3 : X3 ↔ Y3 be
bijections,
∗ : X1 × X2 → X3,
⋆ : Y1 × Y2 → Y3 be
operations. We define
∗ ≃φ1,φ2,φ3 ⋆
by:
(X1 × X2 → X3(x1, x2) ↦ ax1,x2) ≃φ1,φ2,φ3 (Y1 × Y2 → Y3(y1, y2) ↦ by1,y2) :⇔ ∀ x1 ∈ X1, x2 ∈ X2 : φ3(ax1,x2) = bφ1(x1),φ2(x2) (ax1,x2 ∈ X3 for each x1 ∈ X1 and x2 ∈ X2, by1,y2 ∈ Y3 for each y1 ∈ Y1 and y2 ∈ Y2) ⇔ ∀ x1 ∈ X1, x2 ∈ X2 : φ3(x1 ∗ x2) = φ1(x1) ⋆ φ2(x2) ⇔ φ3 ∘ ∗ = ⋆ ∘ (φ1 × φ2) Equivalence. No proof.