let p be XFinSequence; :: thesis: for x being object holds last (p ^ <%x%>) = x
let x be object ; :: thesis: last (p ^ <%x%>) = x
dom (p ^ <%x%>) = len (p ^ <%x%>)
.= (len p) + 1 by Th72
.= (len p) +^ 1 by CARD_2:36
.= succ (len p) by ORDINAL2:31 ;
hence last (p ^ <%x%>) = (p ^ <%x%>) . (len p) by ORDINAL2:6
.= x by Th33 ;
:: thesis: verum