theorem Th72: :: AFINSQ_1:75

for x being object
for p being XFinSequence holds len (p ^ <%x%>) = (len p) + 1