no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.274141
ι' : Sort ?u.274144
ι₂ : Sort ?u.274147
κ : ι → Sort ?u.274152
κ₁ : ι → Sort ?u.274157
κ₂ : ι → Sort ?u.274162
κ' : ι' → Sort ?u.274167
f : β → γ
s : Set (α → β)
t : Set α
⊢ f '' seq s t = seq ((fun x x_1 => x ∘ x_1) f '' s) t
rw [← singleton_seq, ← singleton_seq, seq_seq, image_singleton]