===== Sequence begin =====
==== Function ====
| @#55CCEE: context     | @#55CCEE: $ X $ ... set |

| @#FFBB00: definiendum | @#FFBB00: $ \mathrm{first}: \mathrm{Sequence}(X)\to X $ |
| @#FFBB00: definiendum | @#FFBB00: $ \mathrm{first}(S):= \pi_1(S) $ |

==== Discussion ====
==== Parents ====
=== Subset of ===
[[Surjective function]]
=== Context ===
[[Sequence length]]