How is functional property guaranteed in type theory when function type is defined?
Type theory shows that every element of a function type has the "function property". Let $A$ be a type and $B(x)$ a dependent type with $x : A$. We can construct an element of
$$\Pi (x : A) (y , z : B(x)) \,.\, f x =_{B(x)} y \to f x =_{B(x)} z \to y =_{B(x)} z$$
quite easily, because we just use symmetry and transitivity of equality. For instance in Coq:

Definition functional_property (A : Type) (B : A -&gt; Type) (f : forall x, B x)
  : forall (x : A) (y z : B x) (p : f x = y) (q : f x = z),  y = z
  :=
   fun _ _ _ p q =&gt; eq_trans (eq_sym p) q.


What this means is that, as others already pointed out, the "functional property" is there by construction. It may help to say the following: in type theory we do not think of mathematical objects as existing independently and beforehand. Instead, type theory is a theory of how objects are constructed. Thus, the elements of the function type are constructed in a certain way (known as "$\lambda$-calculus") that guarantees the desired properties by construction. There is no such thing in type theory as "a thing that wants to be a function but isn't because it doesnt have the right properties". That sort of thinking simply does not apply: if you have a thing, then it was constructed according to the rules of some type and therefore the thing has that type.

You are probably thinking set-theoretically, i.e., given a relation $R \subseteq A \times B$, we should be able to get a function out of it, provided that $R$ is single-valued (what you call "functional property") and total. There is a corresponding statement in type theory, but it is not the definition of functions. It is instead a theorem stating that the function type $A \to B$ is equivalent to the type of total functional relations.