theorem Th10: :: AFINSQ_2:10
for p being XFinSequence holds p /^ 0 = p