let D be non empty set ; :: thesis: for f, g being FinSequence of D holds smid (f ^ g),((len f) + 1),((len f) + (len g)) = g
let f, g be FinSequence of D; :: thesis: smid (f ^ g),((len f) + 1),((len f) + (len g)) = g
(((len g) + (len f)) + 1) -' ((len f) + 1) = ((len g) + ((len f) + 1)) -' ((len f) + 1)
.= len g by NAT_D:34 ;
then g | ((((len g) + (len f)) + 1) -' ((len f) + 1)) = g by FINSEQ_1:79;
then ((f ^ g) /^ (len f)) | ((((len f) + (len g)) + 1) -' ((len f) + 1)) = g by FINSEQ_5:40;
hence smid (f ^ g),((len f) + 1),((len f) + (len g)) = g by NAT_D:34; :: thesis: verum