let k be Nat; :: thesis: for p being XFinSequence st len p <= k holds
mid p,1,k = p
let p be XFinSequence; :: thesis: ( len p <= k implies mid p,1,k = p )
assume A1: len p <= k ; :: thesis: mid p,1,k = p
thus mid p,1,k = p | k by Th25
.= p by A1, AFINSQ_1:56 ; :: thesis: verum