for i being natural Number
for D, D9 being non empty set st D = Seg i holds
for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9