∀ {L : FirstOrder.Language} {ι : Type u_3} [inst : Preorder ι] [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  {M : Type u_4} [inst_3 : L.Structure M] (S : ι →o L.Substructure M)
  (liftInclusion_in_sup :
    ∀
      (x :
        FirstOrder.Language.DirectLimit (fun i => ↥(S i)) fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯),
      (FirstOrder.Language.DirectLimit.liftInclusion S) x ∈ ⨆ i, S i)
  {n : ℕ} (f : L.Functions n)
  (x :
    Fin n →
      FirstOrder.Language.DirectLimit (fun i => ↥(S i)) fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯),
  (FirstOrder.Language.Embedding.codRestrict (⨆ i, S i) (FirstOrder.Language.DirectLimit.liftInclusion S)
          liftInclusion_in_sup).toFun
      (FirstOrder.Language.Structure.funMap f x) =
    FirstOrder.Language.Structure.funMap f
      ((FirstOrder.Language.Embedding.codRestrict (⨆ i, S i) (FirstOrder.Language.DirectLimit.liftInclusion S)
            liftInclusion_in_sup).toFun ∘
        x)