theorem :: AFINSQ_1:55

for n being Nat
for p being XFinSequence holds len (p | n) <= n