let f, g be FinSequence; :: thesis: for i being Nat st i <= len f & mid (f,i,((i -' 1) + (len g))) = g holds
(i -' 1) + (len g) <= len f
let i be Nat; :: thesis: ( i <= len f & mid (f,i,((i -' 1) + (len g))) = g implies (i -' 1) + (len g) <= len f )
set j = (i -' 1) + (len g);
assume that
A1: i <= len f and
A2: mid (f,i,((i -' 1) + (len g))) = g ; :: thesis: (i -' 1) + (len g) <= len f

per cases ( i <= (i -' 1) + (len g) or i > (i -' 1) + (len g) ) ;

suppose A3: i <= (i -' 1) + (len g) ; :: thesis: (i -' 1) + (len g) <= len f

then A4: mid (f,i,((i -' 1) + (len g))) = (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by FINSEQ_6:def 3;
A5: i -' 1 <= (len f) -' 1 by A1, NAT_D:42;
(len f) -' 1 <= len f by NAT_D:35;
then i -' 1 <= len f by A5, XXREAL_0:2;
then A6: len (f /^ (i -' 1)) = (len f) - (i -' 1) by RFINSEQ:def 1;

per cases ( i > 0 or i = 0 ) ;

suppose i > 0 ; :: thesis: (i -' 1) + (len g) <= len f

then A8: i -' 1 = i - 1 by NAT_1:14, XREAL_1:233;

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

suppose len g >= 1 ; :: thesis: (i -' 1) + (len g) <= len f

then A10: (len g) - 1 = (len g) -' 1 by XREAL_1:233;
A11: (((- 1) + (len g)) + i) -' i = (- 1) + (len g) by A10, NAT_D:34;
A12: (((i -' 1) + (len g)) -' i) + 1 = len g by A8, A11;

per cases ( len g <= (len f) - (i -' 1) or len g > (len f) - (i -' 1) ) ;

suppose len g <= (len f) - (i -' 1) ; :: thesis: (i -' 1) + (len g) <= len f

then (((i -' 1) + (len g)) + 1) -' i <= (len f) - (i - 1) by A3, A12, A8, NAT_D:38;
then (((i -' 1) + (len g)) + 1) - i <= (len f) - (i - 1) by A3, NAT_D:37;
then ((i -' 1) + (len g)) - (i - 1) <= (len f) - (i - 1) ;
hence (i -' 1) + (len g) <= len f by XREAL_1:9; :: thesis: verum

end;

suppose len g > (len f) - (i -' 1) ; :: thesis: (i -' 1) + (len g) <= len f

then (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) = f /^ (i -' 1) by A6, A12, FINSEQ_1:58;
hence (i -' 1) + (len g) <= len f by A2, A4, A6; :: thesis: verum

end;

end;

end;

suppose len g < 1 ; :: thesis: (i -' 1) + (len g) <= len f

then len g = 0 by NAT_1:14;
then (i -' 1) + (len g) <= i by NAT_D:35;
hence (i -' 1) + (len g) <= len f by A1, XXREAL_0:2; :: thesis: verum

end;

end;

end;

suppose A14: i = 0 ; :: thesis: (i -' 1) + (len g) <= len f

0 -' 1 <= 0 by NAT_D:35;
then A15: i -' 1 = 0 by A14;
A16: (((i -' 1) + (len g)) -' i) + 1 = (len g) + 1 by A14, A15, NAT_D:40;

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

suppose (len g) + 1 <= (len f) - (i -' 1) ; :: thesis: (i -' 1) + (len g) <= len f

then A17: ((i -' 1) + (len g)) + 1 <= len f by A15;
((i -' 1) + (len g)) + 0 <= ((i -' 1) + (len g)) + 1 by XREAL_1:6;
hence (i -' 1) + (len g) <= len f by A17, XXREAL_0:2; :: thesis: verum

end;

suppose (len g) + 1 > (len f) - (i -' 1) ; :: thesis: (i -' 1) + (len g) <= len f

then (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) = f /^ (i -' 1) by A6, A16, FINSEQ_1:58;
hence (i -' 1) + (len g) <= len f by A2, A4, A6; :: thesis: verum

end;

end;

end;

end;

end;

suppose i > (i -' 1) + (len g) ; :: thesis: (i -' 1) + (len g) <= len f

then A20: len g = 0 by Th3;
i -' 1 <= i by NAT_D:35;
hence (i -' 1) + (len g) <= len f by A1, A20, XXREAL_0:2; :: thesis: verum

end;

end;