∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (baseSet : ι → Set B)
  (isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i)) (indexAt : B → ι)
  (mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)) (coordChange : ι → ι → B → F →L[R] F)
  (coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), (coordChange i i x) v = v)
  (continuousOn_coordChange : ∀ (i j : ι), ContinuousOn (coordChange i j) (baseSet i ∩ baseSet j))
  (coordChange_comp :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
        ∀ (v : F), (coordChange j k x) ((coordChange i j x) v) = (coordChange i k x) v)
  (baseSet_1 : ι → Set B) (isOpen_baseSet_1 : ∀ (i : ι), IsOpen (baseSet_1 i)) (indexAt_1 : B → ι)
  (mem_baseSet_at_1 : ∀ (x : B), x ∈ baseSet_1 (indexAt_1 x)) (coordChange_1 : ι → ι → B → F →L[R] F)
  (coordChange_self_1 : ∀ (i : ι), ∀ x ∈ baseSet_1 i, ∀ (v : F), (coordChange_1 i i x) v = v)
  (continuousOn_coordChange_1 : ∀ (i j : ι), ContinuousOn (coordChange_1 i j) (baseSet_1 i ∩ baseSet_1 j))
  (coordChange_comp_1 :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet_1 i ∩ baseSet_1 j ∩ baseSet_1 k,
        ∀ (v : F), (coordChange_1 j k x) ((coordChange_1 i j x) v) = (coordChange_1 i k x) v),
  ({ baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at,
        coordChange := coordChange, coordChange_self := coordChange_self,
        continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } =
      { baseSet := baseSet_1, isOpen_baseSet := isOpen_baseSet_1, indexAt := indexAt_1,
        mem_baseSet_at := mem_baseSet_at_1, coordChange := coordChange_1, coordChange_self := coordChange_self_1,
        continuousOn_coordChange := continuousOn_coordChange_1, coordChange_comp := coordChange_comp_1 }) =
    (baseSet = baseSet_1 ∧ indexAt = indexAt_1 ∧ coordChange = coordChange_1)