∀ x0 x1 x2 . ∀ x3 : ι → ι . equip x0 x1 ⟶ (∀ x4 . x4 ∈ x0 ⟶ equip (x3 x4) x2) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x3 x4 ⟶ x6 ∈ x3 x5 ⟶ x4 = x5) ⟶ equip (famunion x0 x3) (setprod x1 x2) |
|