for p being XFinSequence
for e being object holds dom (p ^ <%e%>) = (dom p) \/ {(card p)}