for U being non empty set
for p being FinSequence st p is U -valued & not p is empty holds
(U -firstChar) . p = p . 1