theorem Th6: :: HELLY:6

for p, q being FinSequence
for j being Nat st j <= len (maxPrefix (p,q)) holds
(maxPrefix (p,q)) . j = p . j