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

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