鳥たちの結合条件

この森の任意の鳥A,Bに対して、任意の鳥xを取れば、Cx = A(Bx)となるような鳥Cがいる。
任意の鳥A,Bに対して,AとBを結合する鳥Cが存在する。

Axiom bird_composition :
forall A B : Bird, 
exists C : Bird,
forall x : Bird,
bird_respond C x = bird_respond A (bird_respond B x).

日本語ってあいまいだなあと思う。