∀ {ι : Type u_5} {B : Type u_6} {inst : TopologicalSpace B} {F : Type u_7} {inst_1 : TopologicalSpace F}
  {baseSet : ι → Set B} {isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i)} {indexAt : B → ι}
  {mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)} {coordChange : ι → ι → B → F → F}
  {coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), coordChange i i x v = v}
  {continuousOn_coordChange :
    ∀ (i j : ι), ContinuousOn (fun p => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ Set.univ)}
  {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 → F}
  {coordChange_self_1 : ∀ (i : ι), ∀ x ∈ baseSet_1 i, ∀ (v : F), coordChange_1 i i x v = v}
  {continuousOn_coordChange_1 :
    ∀ (i j : ι), ContinuousOn (fun p => coordChange_1 i j p.1 p.2) ((baseSet_1 i ∩ baseSet_1 j) ×ˢ Set.univ)}
  {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