Given two sets ~X and ~Y, a #~{function} or #~{map} between them , _ ~f#: ~X -> ~Y _ is defined by a subset _ ~S &subset. ~X # ~Y , _ such that &forall. ~x &in. ~X , &exist. a unique ~y &in. ~Y for which ( ~x , ~y ) &in. ~S . _ (i.e. if ( ~x , ~y' ) &in. ~S also, then ~y' = ~y). We write _ ~f (~x) = ~y.

~X is called the #~{domain} of ~f, and ~Y is called the #~{co-domain}.

The ~#{image} of ~X under ~f is _ ~f (~X) _ = _ \{ ~y &in. ~Y | ~y = ~f (~x) some ~x \}

~Y ~^X represents the set of all functions from ~X to ~Y.

A function _ ~f#: ~X -> ~Y _ is said to be

- #~{injective} or #~{one-to-one} _ if _ ~f (~x) = ~f (~x') _ <=> _ ~x = ~x'
- #~{surjective} or #~{onto} _ if _ &forall. ~y &in. ~Y , &exist. ~x &in. ~X _ such that _ ~y = ~f (~x)
- #~{bijective} _ if it is both injective and surjective.

For any function _ ~f#: ~X -> ~Y , _ the set _ ~f ^{-1} ( ~y ) _ #:= _ \{ ~x | ~f ( ~x ) = ~y \} _ is called the #~{inverse image} of ~y under ~f.

[ Note this defines a map _ ~f ^{-1}#: ~Y -> @P(~X) .]

If ~f is surjective then _ ~f ^{-1} ( ~y ) != &empty. _ for any ~y &in. ~Y.

If ~f is injective then, for any ~y &in. ~Y , either _ ~f ^{-1} ( ~y ) = &empty. _ or _ ~f ^{-1} ( ~y ) = \{ ~x \} _ ( some ~x &in. ~X ).

If ~f is bijective then , for any ~y &in. ~Y , _ &exist. unique ~x &in. ~X _ such that _ ~f ^{-1} ( ~y ) = \{ ~x \}.

In this case define the function _ ~g #: ~Y -> ~X , _ by ~g( ~y ) #:= ~x, _ this is called the #~{inverse function} of ~f , _ and by abuse of notation we write _ ~g = ~f ^{-1}.

Note that ~f ^{-1} is also a bijective function, and that ( ~f ^{-1} ) ^{-1} = ~f.

If _ ~X &subset. ~Y _ we define the #~{inclusion function} _ ~j #: ~X -> ~Y _ by _ ~j ( ~x ) = ~x.

This is an injective function.

We define the #~{identity function} _ ~i_~X #: ~X -> ~X _ by _ ~i_~X ( ~x ) = ~x.

This is a special case of an inclusion map, and is bijective.

Given sets ~X , ~Y , ~Z, and functions ~f#: ~X -> ~Y and ~g#: ~Y -> ~Z , _ then define the #~{composite} function _ ( ~g &comp. ~f ) #: ~X -> ~Z , _ by ( ~g &comp. ~f ) (~x) _ = _ ~g ( ~f (~x) )

Given functions ~f#: ~X -> ~Y , _ ~g#: ~Y -> ~Z _ and ~h#: ~Z -> ~W , we can define the two maps:

- _ _ ~h &comp. ( ~g &comp. ~f ) _ #: ~X -> ~W
- _ _ ( ~h &comp. ~g ) &comp. ~f _ #: ~X -> ~W

In fact these are the same mapping.

Let _ ~f#: ~X -> ~Y , _ where _ ~X != &empty. _ and _ ~Y != &empty. , _ then

- a) _ ~f _ injective _ <=> _ b) _ &exist. ~g #: ~Y -> ~X _ such that _ ~g &comp. ~f = ~i_~X
- c) _ ~f _ surjective _ <=> _ d) _ &exist. ~h #: ~Y -> ~X _ such that _ ~f &comp. ~h = ~i_~Y
- e) _ ~f _ bijective _ <=> _ f) _ &exist. ~k #: ~Y -> ~X _ such that _ ~k &comp. ~f = ~i_~X _ and _ ~f &comp. ~k = ~i_~Y

a) => b) #: _ ~x &in. ~X , _ ~f ( ~x ) = ~y _ say, _ the inverse image of ~y , ~f ^{-1} ( ~y ) = \{ ~x \} (by injectivity). _ Put _ ~g ( ~y ) = ~x _ if ~y &in. ~f (~X ) , _ or _ ~g ( ~y ) = ~x_0 _ otherwise , _ where ~x_0 is any arbitrary element (exists as ~X != &empty.)

then _ ( ~g &comp. ~f ) ( ~x ) = ~x , _ &forall. ~x _ ( including ~x_0 )

b) => a) #: _ ~f ( ~x ) = ~f ( ~x' ) _ => _ ~g &comp. ~f ( ~x ) = ~g &comp. ~f ( ~x' ) => ~i_~X ( ~x ) = ~i_~X ( ~x' ) _ => _ ~x = ~x'

c) => d) #: _ for any _ ~y &in. ~Y , _ let _ ~h ( ~y ) = ~x , _ arbitrary ~x &in. ~f ^{-1} ( ~y ) _ [ &exist. ~x since ~f is surjective ] . _ Then _ ~f &comp. ~h ( ~y ) = ~f ( ~x ) = ~y.

d) => c) #: _ ~f &comp. ~h ( ~y ) = ~y , _ any ~y &in. ~Y _ => _ ~y = ~f ( ~x ) where ~x = ~h ( ~y ) => _ ~f surjective.

e) => f) #: _ We have e) => a) => b) and e) => c) => d), so &exist. ~g and ~h such that ~g &comp. ~f = ~i_~X and ~f &comp. ~h = ~i_~Y ,

but _ ~g _ = _ ~g &comp. ~i_~Y _ = _ ~g &comp. ~f &comp. ~h _ = _ ~i_~X &comp. ~h _ = _ ~h , _ so _ ~g _ = _ ~h _ =#: _ ~k .

f) => e) #: _ Follows immediately from _ b) => a) _ and _ d) => c).

A #~{permutation} is a bijection of a set onto itself.

So by the above, _ ~f #: ~X -> ~X _ is a premutation _ <=> _ &exist. ~g #: ~X -> ~X _ such that _ ~f &comp. ~g _ = _ ~g &comp. ~f.

Obviously ~g is also a permutation.