for D being non empty set
for p, q being FinSequence of D st p c= q holds
ex p9 being FinSequence of D st p ^ p9 = q