let D be non empty set ; :: thesis: for f being FinSequence of D
for k2 being Element of NAT st len f <= k2 holds
smid f,1,k2 = f
let f be FinSequence of D; :: thesis: for k2 being Element of NAT st len f <= k2 holds
smid f,1,k2 = f
let k2 be Element of 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:79 ; :: thesis: verum