let f be FinSequence; :: thesis: for k2 being Nat holds smid (f,1,k2) = f | k2
let k2 be Nat; :: thesis: smid (f,1,k2) = f | k2
thus smid (f,1,k2) = (f /^ 0) | ((k2 + 1) -' 1) by NAT_2:8
.= f | ((k2 + 1) -' 1) by FINSEQ_5:28
.= f | k2 by NAT_D:34 ; :: thesis: verum