Formalize function application and describe its notation in pure lambda calculus?

Function application is called a Beta-redex/Reducible expression in pure lambda calculus.

Notation: $t_1{t}_2$ in which $t_1$ is a lambda abstraction.