Added an axiom: finiteness of words.

To be removed and proven once Arthur makes the actual change to finite words.