:: deftheorem defines plus-one DTCONSTR:def 7 :
for x being FinSequence of NAT holds plus-one x = (x . 1) + 1;