theorem :: AFINSQ_1:52

for n being Nat
for p being XFinSequence st len p <= n holds
p | n = p