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