Is proving $(f: X→ Y)\land f(\varnothing)\neq\varnothing$ is a contradiction correct in the proof of this statement? 
Definition 4
  The connective $\rightarrow$ is called the conditional and may be placed between any two statement $p$ and $q$ to form the compound statement $p→q$ (read: "if $p$, then $q$". By definition the statement $p→q$ is equivalent to the statement $\sim(p∧\sim q)$.
Definition 8. Let $X$ and $Y$ be sets. A function from $X$ to $Y$ is a triple $(f, X, Y)$, where $f$ is a relation from $X$ to $Y$ satisfying
  (a) $\operatorname{Dom}(f) = X$.
  (b) If $(x, y) \in f$ and $(x, z) \in f$, then $y=z$.
  We shall adhere to the custom of writing $f: X\space \rightarrow Y$ instead of $(f, X, Y)$ and $y=f(x)$ instead of $(x,\space y) \in f$.  
Definition 9 Let: $X\rightarrow Y$ be a function, and let $A$ and $B$ be subsets of X and Y, respectively.
(a) The image of $A$ under $f$, which we denote $f(A)$, is the set of all images $f(x)$ such that $x∈A$.
  (b) The inverse image of B under f, which we denote $f^{-1}(B)$, is the set of all images of y in B.

In symbols, $f (A) =\{ f (x) \mid x\in A\}$,   $f^{-1}(B)=\{x \mid f (x)\in B\}$

"Theorem 9 (a) Let $f: X\rightarrow Y$. Then $f(\varnothing)=\varnothing$"
  Source: Set Theory, You-Feng Lin, Shwu-Yeng T. Lin    

The author leaves the proof of the theorem 9 to the reader. So I completed the proof by reductio ad absurdum, but I'm not sure if proving $(f: X→ Y)\land f(\varnothing)\neq \varnothing$ is a contradiction done correctly.
[My trial of proof of Theorem 9(a) by contradiction]
Let's start by negation of the statement.
$$\sim [(f: X\rightarrow Y)\rightarrow f(\varnothing)=\varnothing ]≡ \\
[(f: X\rightarrow Y)\land \sim [f(\varnothing)=\varnothing]]≡ \\  
\color{red}{[(f: X\rightarrow Y)\land} [\color{red}{f(\varnothing)\neq \varnothing} ]] $$
However, in $f(\varnothing) = \{f (x) \mid x\in \varnothing\}$, $x∈\varnothing$ is a contradiction.
Thus $[f(\varnothing)\neq \varnothing ]]≡ c\neq \varnothing ≡ c$   
It's proved that $[(f: X\rightarrow Y)\Rightarrow f(\varnothing)=\varnothing ]$
Q.E.D
[Added, proof modified]
$f(Ø)≠Ø $
$⇔∃y, y∈f(Ø)$
$⇔y=f(x)∧x∈Ø$
$⇔c$   since x∈Ø is a contradiction.
Done. 
Q.E.D.
 A: Your proof doesn't really get to the meat of the matter. The main fallacy you're committing is at

However, in $f(\varnothing) = \{f (x) \mid x\in \varnothing\}$, $x∈\varnothing$ is a contradiction.

This doesn't work to conclude your proof by contradiction. It is true that somewhere on the paper you can now see the known false claim $x\in\varnothing$, but in order to conclude the proof-by-contradiction you have started, it is not enough for a contradicton to be on the paper -- it needs to be something that you have concluded would be true if your assumptions hold.
And in this case, what you have concluded is true is the whole formula
$$ f(\varnothing) = \{f(x)\mid x\in\varnothing\}  $$
The fact that this has "something that is always false" inside it doesn't make the claim itself "always false". As a simpler example, the formula
$$ \sim(1=0) $$
is a perfectly good truth even though it contains the contradiction $1=0$.

In general, your proof attempts wastes a lot of energy manipulating the assumption $f:X\to Y$. That's somewhat besides the point here and not what is done in mathematical proofs in general. Usually we just say something like

Theorem. Assume $P$. Then $Q$.
Proof. I will prove $Q$ by contradiction, so assume $\sim Q$. Then (bla bla bla bla) and we assumed $\sim Q$ and therefore (bla bla bla bla) and we assumed $P$ and therefore (bla bla bla bla) which is a contradiction. Therefore $Q$, q.e.d.

The manipulation you show is one way to justify this trope, but it's not something you would state from first principles each time you write down a proof. (That would just lead to your forest being invisible for trees). If you want to fully formalize your proof (which it doesn't look like you have all the tools to do yet), it may or may not be necessary to do something like what you're doing there, as part of the formalization. But most formal proof systems wouldn't even need that -- they have other ways of representing the reasoning above.

Finally, what you actually should have done:
Forget about the assumption $f:X\to Y$. You're not going to need it; the only reason it's in the statement of the theorem is such that it is allowed to write the notation $f(\varnothing)$ later in the statement of the theorem.
Instead we can prove directly that $f(\varnothing)=\varnothing$ by letting $y$ be arbitary and show that $\sim(y\in f(\varnothing))$ (because that's what it means for a set to be $\varnothing$).
By definition of $f(A)$, the subformula $y\in f(\varnothing)$ is an abbreviation for
$$ \exists x ( x\in \varnothing \land f(x)=y ) $$
and this is always false because $x\in \varnothing$ is false, which makes the existentially quantified formula false no matter what $x$ or $f$ or $y$ is.
Therefore $\sim(y\in f(\varnothing))$ and we're done.
