let D be set ; :: thesis: for f being XFinSequence of
for k2 being Nat st len f <= k2 holds
mid f,1,k2 = f
let f be XFinSequence of ; :: thesis: for k2 being Nat st len f <= k2 holds
mid f,1,k2 = f
let k2 be Nat; :: thesis: ( len f <= k2 implies mid f,1,k2 = f )
assume A1: len f <= k2 ; :: thesis: mid f,1,k2 = f
thus mid f,1,k2 = f | k2 by Th25
.= f by A1, Th10 ; :: thesis: verum