theorem Th6: :: AFINSQ_2:6

for n being Nat
for p being XFinSequence st n >= len p holds
p /^ n = {}