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