Sequence begin
Function
context
$ X $ … set
definiendum
$ \mathrm{first}: \mathrm{Sequence}(X)\to X $
definiendum
$ \mathrm{first}(S):= \pi_1(S) $
Discussion
Parents
Subset of
Surjective function
Context
Sequence length