Given $f$ as an invertible function with domain $X$ and codomain $Y$, then we can say
$$f^{-1}(f(x)) = x $$
Or since they are both logically equivalent
$$ f(f^{-1}(x)) = x $$
This can also be written more formally as :
$$f^{-1} \circ f = id_x \ \Leftrightarrow f \circ f^{-1} = id_x $$
It is a relatively simple and common, property of functions, yet I haven't seen a formal proof of it. So how do you prove this statement $\ \forall f\ $, where $f$ is an arbitrary invertible function?
If the proof requires higher mathematics (e.g Category Theory, Morphisms etc.), please do not hesitate to include them.
It is the definition of an invertible function.
A function $f:X\to Y$ is said to be invertible if there exists a function $g:Y\to X$ such that
$$\forall y \in Y, f(g(y)) = y \text{ and } \forall x\in X, g(f(x)) = x$$
If $f$ has this property, we call $g$ the inverse of $f$ and note it $f^{-1}:= g$