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

| @#FFBB00: definiendum | @#FFBB00: $ \mathrm{last}: \mathrm{FiniteSequence}(X)\to X $ |
| @#FFBB00: definiendum | @#FFBB00: $ \mathrm{last}(S):= \pi_{\mathrm{length}(S)}(S) $ |

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