let x be object ; :: thesis: for p being XFinSequence holds len (p ^ <%x%>) = (len p) + 1
let p be XFinSequence; :: thesis: len (p ^ <%x%>) = (len p) + 1
thus len (p ^ <%x%>) = (len p) + (len <%x%>) by Def3
.= (len p) + 1 by Th30 ; :: thesis: verum