let f be FinSequence; :: thesis: for k2 being Nat st len f <= k2 holds
smid (f,1,k2) = f
let k2 be Nat; :: thesis: ( len f <= k2 implies smid (f,1,k2) = f )
assume A1: len f <= k2 ; :: thesis: smid (f,1,k2) = f
thus smid (f,1,k2) = f | k2 by Th5
.= f by A1, FINSEQ_1:58 ; :: thesis: verum