∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂}
  {A₁ : (i : ι₁) → Set (R₁ i)} {A₂ : (i : ι₂) → Set (R₂ i)} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁)
  (φ : (j : ι₂) → R₁ (f j) → R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo (φ j) (A₁ (f j)) (A₂ j))
  (x : RestrictedProduct (fun i => R₁ i) (fun i => A₁ i) 𝓕₁) (j : ι₂),
  (RestrictedProduct.mapAlong R₁ R₂ f hf φ hφ x) j = φ j (x (f j))