For any sets , , can form The unique (by (Ext)) is denoted by We write for Formally, we introduced a binary symbol and a unary symbol By (Ext) we have We can now define Ordered Pair and Function