∀ {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [inst : TopologicalSpace A]
  [inst_1 : (i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)),
  (ContinuousMap.piEquiv A X) f = ContinuousMap.pi f