for D being non empty set
for p, q being FinSequence of D
for i being Element of NAT st p c= q & 1 <= i & i <= len p holds
q . i = p . i