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:58 ; :: thesis: verum