let D be non empty set ; :: thesis: for f, g being FinSequence of D st len g >= 1 holds
mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g
let f, g be FinSequence of D; :: thesis: ( len g >= 1 implies mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g )
assume A1: len g >= 1 ; :: thesis: mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g
A2: g | (len g) = g | (Seg (len g)) by FINSEQ_1:def 16;

per cases ( (len f) + 1 <= (len f) + (len g) or (len f) + 1 > (len f) + (len g) ) ;

suppose A3: (len f) + 1 <= (len f) + (len g) ; :: thesis: mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g

then A4: len f < (len f) + (len g) by NAT_1:13;
then (len f) - (len f) < ((len f) + (len g)) - (len f) by XREAL_1:14;
then A5: ((len f) + (len g)) -' (len f) = len g by XREAL_0:def 2;
mid ((f ^ g),((len f) + 1),((len f) + (len g))) = ((f ^ g) /^ (((len f) + 1) -' 1)) | ((((len f) + (len g)) -' ((len f) + 1)) + 1) by A3, FINSEQ_6:def 3
.= ((f ^ g) /^ (len f)) | ((((len f) + (len g)) -' ((len f) + 1)) + 1) by NAT_D:34
.= ((f ^ g) /^ (len f)) | (((len f) + (len g)) -' (len f)) by A4, NAT_2:7
.= g | (len g) by A5 ;
hence mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g by A2, FINSEQ_2:20; :: thesis: verum

end;

suppose (len f) + 1 > (len f) + (len g) ; :: thesis: mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g

then ((len f) + 1) - (len f) > ((len f) + (len g)) - (len f) by XREAL_1:14;
hence mid ((f ^ g),((len f) + 1),((len f) + (len g))) = g by A1; :: thesis: verum

end;

end;