theorem Th7: :: HELLY:7

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