let p be XFinSequence; :: thesis: for e being object holds dom (p ^ <%e%>) = (dom p) \/ {(card p)}
let e be object ; :: thesis: dom (p ^ <%e%>) = (dom p) \/ {(card p)}
thus dom (p ^ <%e%>) = dom (p +* (Shift (<%e%>,(card p)))) by Th74
.= (dom p) \/ (dom (Shift (<%e%>,(card p)))) by FUNCT_4:def 1
.= (dom p) \/ {(card p)} by Th84 ; :: thesis: verum