English
The associativity of the seq operation: s.seq(t.seq(u)) equals seq of seq composition applied to s and t then u.
Русский
Ассоциативность операции seq: s.seq(t.seq(u)) = seq((∘)''s ∘ t) u.
LaTeX
$$$$ \\operatorname{seq} s (\\operatorname{seq} t u) = \\operatorname{seq} (\\operatorname{seq} ((\\cdot \\circ \\cdot) '' s) t) u $$$$
Lean4
theorem seq_seq {s : Set (β → γ)} {t : Set (α → β)} {u : Set α} : seq s (seq t u) = seq (seq ((· ∘ ·) '' s) t) u :=
by
simp only [seq_eq_image2, image2_image_left]
exact .symm <| image2_assoc fun _ _ _ ↦ rfl