theorem Th51: :: AFINSQ_1:54

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