intro z
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
⊢ ∀ (x : γ), x ∈ g.seq (f.seq s) ↔ x ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
⊢ z ∈ g.seq (f.seq s) ↔ z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s