Observation. Loop space of FinSet_n [00DF]

The groupoid of finite sets with cardinality , is pointed connected with base point . Its loop space is the symmetric group .

In other words

Proof. TODO.