theorem Th32: :: AFINSQ_1:35

for x being object
for p being XFinSequence holds (<%x%> ^ p) . 0 = x