« Species on FinSet and action types

Lemma. [00DE]

By Lemma 2.24.4 we get that

Backlinks

[00DG]

Consider a species . By this and by this, restricts to

In other words, is given precisely by what is does on each , since