for n being non zero Nat
for f being NtoSEG Function of (Segm n),(Seg n)
for i being Nat st i < n holds
( f . i = i + 1 & i in dom f )