theorem :: AFINSQ_1:89

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