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 15;

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:16;
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, JORDAN3:def 1
.= ((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:9
.= g | (len g) by A5, FINSEQ_5:40 ;
hence mid (f ^ g),((len f) + 1),((len f) + (len g)) = g by A2, FINSEQ_2:23; :: 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:16;
hence mid (f ^ g),((len f) + 1),((len f) + (len g)) = g by A1; :: thesis: verum

end;

end;