X /\ Y → Z
set set set
definition
let X , Y be set;
func X /\ Y -> set
means
:N: x in it iff
x in X & x in Y;
existence ......;
uniqueness
proof
end;
end;
この場合も，
という関数定義でなく，演算子の形で書けます．
，こういう記号を定義したいとします．集合 X と集合 Y からあたらしい集合 Z を作り出す，それがまさにこの functor です．let X, Y be set; で，集合 X, Y を用意します．func X /\ Y → setで，X /\ Y が set であるということを表わしています．means の次の行が，その functor の意味です．先程と同じ様にラベルをつけて，functor の意味を書きます．この意味中で，X /\ Y を it と置きます．そして，証明部(意味の内容)では，existence (存在)と uniqueness (ユニーク)の証明をしなければいけません．存在して，かつユニークであることをいわなくてはいけないわけです．
uniqueness の証明のしかたですが，以下のことを言えばいいわけです．
itとして A1, A2 を取ってくると，
(x in A1 ⇔ x in X & x in Y)
かつ (x in A2 ⇔ x in X & x in Y)
⇒ A1 = A2
これを書くと，
uniqueness
proof
let A1,A2 be set such that
A1: x in A1 iff x in X & x in Y
and
A2: x in A2 iff x in X & x in Y;
now let y;
y in A1 iff y in X & y in Y by A1;
hence y in A1 iff y in A2 by A2;
end:
hence A1=A2 by TARSKI:2;
というふうになります．つまり，この条件をみたす集合2つ A1, A2 をとってくると，実はそれらは等しいということを証明することで uniqueness を証明したことになります．
この uniqueness の証明の中で，まず，3行目に such that がありますから，そのあとに2つの文，ラベル A1 文とラベル A2 文が and で結ばれていることがわかります．そして now let y となっています．この y は set であることが reserve されているとします．そして，ラベル A1 より，y in A1 iff y in X & y in Y であることが言えて，さらに，このこととラベル A2 より，y in A1 iff y in A2 であることが言えるわけです．そして，A1=A2であるための必要十分条件は任意の y に対して，y in A1 と y in A2 が同値であるという，TARSKI:2 より，A1=A2 が証明されたわけです．
existence も同様ですが，こういう it が存在するということを証明します．すなわち，
ex A being set st for x
holds x in A1 iff x in X & x in Y
を証明します．