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:10
.= f | ((k2 + 1) -' 0 ) by FINSEQ_5:31
.= 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:31
.= smid f,1,(k2 + 1) by NAT_2:10 ; :: thesis: verum