Composite function by definition

I found this expression on Wikipedia:

If $\displaystyle f: X \rightarrow Y$, then $\displaystyle f \circ id_X = id_Y \circ f$,

where $\displaystyle id_X$ and $\displaystyle id_Y$ are identity functions.

I wanted to see whether it's true. So I rewrite the expression using the definition of composite function.

Definition:
$\displaystyle
(g \circ f)(x)=g(f(x))=g(y)=z
$ for $\displaystyle f:X \rightarrow Y$, $\displaystyle g: Y \rightarrow Z$, $\displaystyle x \in X, y \in Y$, and $\displaystyle z \in Z$.

I replaced $\displaystyle f$ with $\displaystyle g$ in $\displaystyle f \circ id_X$ and replaced $\displaystyle id_X$ with $\displaystyle f(x)=x$, where $\displaystyle x \in X$. So I wrote the expression for the LHS

Let $\displaystyle f:X\rightarrow X$ and $\displaystyle g:x\rightarrow Y$, where $\displaystyle x\in X $and $\displaystyle y \in Y$.

$\displaystyle
g\circ id = (g\circ f)(x)=g(f(x))=g(x)=y= g
$, but now my difficulty being that I don't know how to express the RHS

$\displaystyle
id_Y \circ g =?
$

I can't find any information anywhere on the web proving $\displaystyle f \circ id_X = id_Y \circ f$.

Could someone please show me how to write the expression for the RHS?

Quote:

---

Originally Posted by novice

If $\displaystyle f: X \rightarrow Y$, then $\displaystyle f \circ id_X = id_Y \circ f$,
where $\displaystyle id_X$ and $\displaystyle id_Y$ are identity functions.

---

Use $\displaystyle i_X~\&~i_Y$ for the identity functions.
The by definition if $\displaystyle (p,q)\in f\circ i_X$ then $\displaystyle \left( {\exists r} \right)\left[ {(p,r) \in i_X \wedge (r,q) \in f} \right]$
But $\displaystyle (p,r) \in i_X $ implies $\displaystyle p=r$. So $\displaystyle (p,q) \in f$.

If $\displaystyle (p,q)\in i_Y\circ f$ then $\displaystyle \left( {\exists s} \right)\left[ {(p,s) \in f \wedge (s,q) \in i_Y} \right]$.
$\displaystyle (s,q) \in i_Y $ implies that $\displaystyle s=q$, so $\displaystyle (p,q)\in f$.

Does that help?

That is so clever.(Clapping)