theorem Th1: :: SPRECT_5:1

for D being non empty set
for f being FinSequence of D
for p, q being Element of D st q in rng (f | (p .. f)) holds
q .. f <= p .. f