English
If s and t are finite, then the image2 of f over s and t is finite.
Русский
Если s и t конечны, то image2 f s t конечен.
LaTeX
$$$ \forall f : \alpha \to \beta \to \gamma,\; s.Finite \land t.Finite \Rightarrow (image2\ f\ s\ t).Finite $$$
Lean4
protected theorem image2 (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) : (image2 f s t).Finite :=
by
have := hs.to_subtype
have := ht.to_subtype
apply toFinite