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 Th16
.= p by A1, AFINSQ_1:52 ; :: thesis: verum