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