let D be non empty set ; :: thesis: for f being FinSequence of D
for k2 being Element of NAT holds smid f,1,k2 = f | k2
let f be FinSequence of D; :: thesis: for k2 being Element of NAT holds smid f,1,k2 = f | k2
let k2 be Element of NAT ; :: thesis: smid f,1,k2 = f | k2
thus smid f,1,k2 = (f /^ 0 ) | ((k2 + 1) -' 1) by NAT_2:10
.= f | ((k2 + 1) -' 1) by FINSEQ_5:31
.= f | k2 by NAT_D:34 ; :: thesis: verum