let x be set ; :: 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 Th20
.= (len p) + 1 by Th36 ; :: thesis: verum