let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} implies f ^ (mid g,2,(len g)) is being_S-Seq )
assume that
A1: f . (len f) = g . 1 and
A2: f is being_S-Seq and
A3: g is being_S-Seq and
A4: (L~ f) /\ (L~ g) = {(g . 1)} ; :: thesis: f ^ (mid g,2,(len g)) is being_S-Seq
A5: len f >= 2 by A2, TOPREAL1:def 10;
A6: len (f ^ (mid g,2,(len g))) = (len f) + (len (mid g,2,(len g))) by FINSEQ_1:35;
then len f <= len (f ^ (mid g,2,(len g))) by NAT_1:11;
then A7: len (f ^ (mid g,2,(len g))) >= 2 by A5, XXREAL_0:2;
A8: len g >= 2 by A3, TOPREAL1:def 10;
then A9: 1 <= len g by XXREAL_0:2;
then A10: len (mid g,2,(len g)) = ((len g) -' 2) + 1 by A8, Th27
.= ((len g) - 2) + 1 by A8, XREAL_1:235
.= (len g) - 1 ;
for x1, x2 being set st x1 in dom (f ^ (mid g,2,(len g))) & x2 in dom (f ^ (mid g,2,(len g))) & (f ^ (mid g,2,(len g))) . x1 = (f ^ (mid g,2,(len g))) . x2 holds
x1 = x2

proof

A11: rng g c= L~ g by A8, SPPOL_2:18;
A12: rng (f ^ (mid g,2,(len g))) c= the carrier of (TOP-REAL 2) by FINSEQ_1:def 4;
let x1, x2 be set ; :: thesis: ( x1 in dom (f ^ (mid g,2,(len g))) & x2 in dom (f ^ (mid g,2,(len g))) & (f ^ (mid g,2,(len g))) . x1 = (f ^ (mid g,2,(len g))) . x2 implies x1 = x2 )
assume that
A13: x1 in dom (f ^ (mid g,2,(len g))) and
A14: x2 in dom (f ^ (mid g,2,(len g))) and
A15: (f ^ (mid g,2,(len g))) . x1 = (f ^ (mid g,2,(len g))) . x2 ; :: thesis: x1 = x2
reconsider n1 = x1, n2 = x2 as Element of NAT by A13, A14;
A16: x2 in Seg (len (f ^ (mid g,2,(len g)))) by A14, FINSEQ_1:def 3;
then A17: 1 <= n2 by FINSEQ_1:3;
(f ^ (mid g,2,(len g))) . x1 in rng (f ^ (mid g,2,(len g))) by A13, FUNCT_1:def 5;
then reconsider q = (f ^ (mid g,2,(len g))) . x1 as Point of (TOP-REAL 2) by A12;
A18: rng (mid g,2,(len g)) c= rng g by Th28;
A19: rng f c= L~ f by A5, SPPOL_2:18;

A20: now

A21: now

g | 1 = g | (Seg 1) by FINSEQ_1:def 15;
then A22: (g | 1) . 1 = g . 1 by FINSEQ_1:5, FUNCT_1:72;
len (g | 1) = 1 by A8, FINSEQ_1:80, XXREAL_0:2;
then 1 in dom (g | 1) by FINSEQ_3:27;
then A23: g . 1 in rng (g | 1) by A22, FUNCT_1:def 5;
A24: 2 -' 1 = 2 - 1 by XREAL_1:235;
assume g . 1 in rng (mid g,2,(len g)) ; :: thesis: contradiction
then A25: g . 1 in rng (g /^ 1) by A8, A24, Th26;
rng (g | 1) misses rng (g /^ 1) by A3, FINSEQ_5:37;
hence contradiction by A25, A23, XBOOLE_0:3; :: thesis: verum

end;

assume that
A26: q in rng f and
A27: q in rng (mid g,2,(len g)) ; :: thesis: contradiction
q in rng g by A18, A27;
then q in (L~ f) /\ (L~ g) by A19, A11, A26, XBOOLE_0:def 4;
hence contradiction by A4, A27, A21, TARSKI:def 1; :: thesis: verum

end;

n2 <= len (f ^ (mid g,2,(len g))) by A16, FINSEQ_1:3;
then A28: n2 - (len f) <= ((len f) + (len (mid g,2,(len g)))) - (len f) by A6, XREAL_1:11;
A29: x1 in Seg (len (f ^ (mid g,2,(len g)))) by A13, FINSEQ_1:def 3;
then n1 <= len (f ^ (mid g,2,(len g))) by FINSEQ_1:3;
then A30: n1 - (len f) <= ((len f) + (len (mid g,2,(len g)))) - (len f) by A6, XREAL_1:11;
A31: 1 <= n1 by A29, FINSEQ_1:3;

now

per cases ( n1 <= len f or n1 > len f ) ;

case n1 <= len f ; :: thesis: x1 = x2

then A32: n1 in dom f by A31, FINSEQ_3:27;
then A33: (f ^ (mid g,2,(len g))) . x1 = f . n1 by FINSEQ_1:def 7;

now

per cases ( n2 <= len f or n2 > len f ) ;

case n2 <= len f ; :: thesis: x1 = x2

then A34: n2 in dom f by A17, FINSEQ_3:27;
then (f ^ (mid g,2,(len g))) . x2 = f . n2 by FINSEQ_1:def 7;
hence x1 = x2 by A2, A15, A32, A33, A34, FUNCT_1:def 8; :: thesis: verum

end;

case A35: n2 > len f ; :: thesis: contradiction

then (len f) + 1 <= n2 by NAT_1:13;
then A36: ((len f) + 1) - (len f) <= n2 - (len f) by XREAL_1:11;
then A37: 1 <= n2 -' (len f) by NAT_D:39;
A38: (len f) + (n2 -' (len f)) = (len f) + (n2 - (len f)) by A35, XREAL_1:235
.= n2 ;
n2 -' (len f) <= len (mid g,2,(len g)) by A28, A36, NAT_D:39;
then A39: n2 -' (len f) in dom (mid g,2,(len g)) by A37, FINSEQ_3:27;
then (f ^ (mid g,2,(len g))) . ((len f) + (n2 -' (len f))) = (mid g,2,(len g)) . (n2 -' (len f)) by FINSEQ_1:def 7;
hence contradiction by A15, A20, A32, A33, A39, A38, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

case A40: n1 > len f ; :: thesis: x1 = x2

then (len f) + 1 <= n1 by NAT_1:13;
then A41: ((len f) + 1) - (len f) <= n1 - (len f) by XREAL_1:11;
then A42: 1 <= n1 -' (len f) by NAT_D:39;
then A43: 1 <= (n1 -' (len f)) + 1 by NAT_D:48;
n1 -' (len f) <= (n1 -' (len f)) + 2 by NAT_1:11;
then A44: ((n1 -' (len f)) + 2) -' 1 = ((n1 -' (len f)) + 2) - 1 by A42, XREAL_1:235, XXREAL_0:2
.= (n1 -' (len f)) + ((1 + 1) - 1) ;
A45: (len f) + (n1 -' (len f)) = (len f) + (n1 - (len f)) by A40, XREAL_1:235
.= n1 ;
A46: n1 -' (len f) <= len (mid g,2,(len g)) by A30, A41, NAT_D:39;
then A47: n1 -' (len f) in dom (mid g,2,(len g)) by A42, FINSEQ_3:27;
then A48: (f ^ (mid g,2,(len g))) . ((len f) + (n1 -' (len f))) = (mid g,2,(len g)) . (n1 -' (len f)) by FINSEQ_1:def 7;
(n1 -' (len f)) + 1 <= ((len g) - 1) + 1 by A10, A46, XREAL_1:8;
then A49: (n1 -' (len f)) + 1 in dom g by A43, FINSEQ_3:27;
(len f) + (n1 -' (len f)) = (len f) + (n1 - (len f)) by A40, XREAL_1:235
.= n1 ;
then A50: (f ^ (mid g,2,(len g))) . n1 = g . ((n1 -' (len f)) + 1) by A8, A9, A30, A41, A48, A44, Th27;

now

per cases ( n2 <= len f or n2 > len f ) ;

case n2 <= len f ; :: thesis: contradiction

then A51: n2 in dom f by A17, FINSEQ_3:27;
then (f ^ (mid g,2,(len g))) . x2 = f . n2 by FINSEQ_1:def 7;
hence contradiction by A15, A20, A47, A48, A45, A51, FUNCT_1:def 5; :: thesis: verum

end;

case A52: n2 > len f ; :: thesis: x1 = x2

then (len f) + 1 <= n2 by NAT_1:13;
then A53: ((len f) + 1) - (len f) <= n2 - (len f) by XREAL_1:11;
then A54: 1 <= n2 -' (len f) by NAT_D:39;
then A55: 1 <= (n2 -' (len f)) + 1 by NAT_D:48;
A56: n2 -' (len f) <= len (mid g,2,(len g)) by A28, A53, NAT_D:39;
then (n2 -' (len f)) + 1 <= ((len g) - 1) + 1 by A10, XREAL_1:8;
then A57: (n2 -' (len f)) + 1 in dom g by A55, FINSEQ_3:27;
n2 -' (len f) <= (n2 -' (len f)) + 2 by NAT_1:11;
then A58: ((n2 -' (len f)) + 2) -' 1 = ((n2 -' (len f)) + 2) - 1 by A54, XREAL_1:235, XXREAL_0:2
.= (n2 -' (len f)) + 1 ;
1 <= n2 -' (len f) by A53, NAT_D:39;
then n2 -' (len f) in dom (mid g,2,(len g)) by A56, FINSEQ_3:27;
then A59: (f ^ (mid g,2,(len g))) . ((len f) + (n2 -' (len f))) = (mid g,2,(len g)) . (n2 -' (len f)) by FINSEQ_1:def 7;
(len f) + (n2 -' (len f)) = (len f) + (n2 - (len f)) by A52, XREAL_1:235
.= n2 ;
then (f ^ (mid g,2,(len g))) . n2 = g . ((n2 -' (len f)) + 1) by A8, A9, A28, A53, A59, A58, Th27;
then (n1 -' (len f)) + 1 = (n2 -' (len f)) + 1 by A3, A15, A49, A50, A57, FUNCT_1:def 8;
then n1 - (len f) = n2 -' (len f) by A40, XREAL_1:235;
then n1 - (len f) = n2 - (len f) by A52, XREAL_1:235;
hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

then A60: f ^ (mid g,2,(len g)) is one-to-one by FUNCT_1:def 8;
A61: 1 <= len f by A5, XXREAL_0:2;
A62: for i, j being Nat st i + 1 < j holds
LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j

proof

let i, j be Nat; :: thesis: ( i + 1 < j implies LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j )
assume A63: i + 1 < j ; :: thesis: LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j

now

per cases ( ( j < len f & j + 1 <= len (f ^ (mid g,2,(len g))) ) or ( i + 1 <= len f & len f <= j & j + 1 <= len (f ^ (mid g,2,(len g))) ) or ( len f < i + 1 & j + 1 <= len (f ^ (mid g,2,(len g))) ) or j + 1 > len (f ^ (mid g,2,(len g))) ) ;

case A64: ( j < len f & j + 1 <= len (f ^ (mid g,2,(len g))) ) ; :: thesis: LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j

then A65: i + 1 < len f by A63, XXREAL_0:2;
then A66: i < len f by NAT_1:13;
A67: j <= len (f ^ (mid g,2,(len g))) by A64, NAT_D:46;
then A68: i + 1 < len (f ^ (mid g,2,(len g))) by A63, XXREAL_0:2;
then A69: i <= len (f ^ (mid g,2,(len g))) by NAT_D:46;

now

per cases ( 1 <= i or i < 1 ) ;

case A70: 1 <= i ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

then A71: f /. i = f . i by A66, FINSEQ_4:24;
(f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A69, A70, FINSEQ_4:24;
then A72: (f ^ (mid g,2,(len g))) /. i = f /. i by A66, A70, A71, FINSEQ_1:85;
A73: LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f ^ (mid g,2,(len g))),i by A68, A70, TOPREAL1:def 5;
A74: 1 <= i + 1 by A70, NAT_D:48;
then A75: f /. (i + 1) = f . (i + 1) by A65, FINSEQ_4:24;
(f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A68, A74, FINSEQ_4:24;
then LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f /. i),(f /. (i + 1)) by A65, A74, A72, A75, FINSEQ_1:85;
then A76: LSeg (f ^ (mid g,2,(len g))),i = LSeg f,i by A65, A70, A73, TOPREAL1:def 5;
A77: 1 < j by A63, A74, XXREAL_0:2;
then A78: f /. j = f . j by A64, FINSEQ_4:24;
(f ^ (mid g,2,(len g))) /. j = (f ^ (mid g,2,(len g))) . j by A67, A77, FINSEQ_4:24;
then A79: (f ^ (mid g,2,(len g))) /. j = f /. j by A64, A77, A78, FINSEQ_1:85;
A80: 1 <= j + 1 by A77, NAT_D:48;
then A81: (f ^ (mid g,2,(len g))) /. (j + 1) = (f ^ (mid g,2,(len g))) . (j + 1) by A64, FINSEQ_4:24;
A82: j + 1 <= len f by A64, NAT_1:13;
then A83: LSeg f,j = LSeg (f /. j),(f /. (j + 1)) by A77, TOPREAL1:def 5;
f /. (j + 1) = f . (j + 1) by A80, A82, FINSEQ_4:24;
then A84: LSeg ((f ^ (mid g,2,(len g))) /. j),((f ^ (mid g,2,(len g))) /. (j + 1)) = LSeg (f /. j),(f /. (j + 1)) by A80, A82, A79, A81, FINSEQ_1:85;
LSeg ((f ^ (mid g,2,(len g))) /. j),((f ^ (mid g,2,(len g))) /. (j + 1)) = LSeg (f ^ (mid g,2,(len g))),j by A64, A77, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j by A2, A63, A76, A84, A83, TOPREAL1:def 9;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} by XBOOLE_0:def 7; :: thesis: verum

end;

case i < 1 ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

then LSeg (f ^ (mid g,2,(len g))),i = {} by TOPREAL1:def 5;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} ; :: thesis: verum

end;

end;

end;

hence LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j by XBOOLE_0:def 7; :: thesis: verum

end;

case A85: ( i + 1 <= len f & len f <= j & j + 1 <= len (f ^ (mid g,2,(len g))) ) ; :: thesis: LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j

now

per cases ( ( i + 1 < len f & len f <= j ) or ( i + 1 <= len f & len f < j ) ) by A63, A85, XXREAL_0:1;

case A86: ( i + 1 < len f & len f <= j ) ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

len f <= (len f) + (len (mid g,2,(len g))) by NAT_1:11;
then A87: i + 1 < len (f ^ (mid g,2,(len g))) by A6, A86, XXREAL_0:2;
A88: len f <= j + 1 by A86, NAT_D:48;
A89: 1 + 1 <= j by A5, A86, XXREAL_0:2;
then A90: 1 <= j by NAT_D:46;

now

per cases ( 1 <= i or i < 1 ) ;

case A91: 1 <= i ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

i <= len f by A85, NAT_D:46;
then A92: f /. i = f . i by A91, FINSEQ_4:24;
i <= len (f ^ (mid g,2,(len g))) by A87, NAT_D:46;
then A93: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A91, FINSEQ_4:24;
i <= len f by A85, NAT_D:46;
then A94: (f ^ (mid g,2,(len g))) /. i = f /. i by A91, A93, A92, FINSEQ_1:85;
A95: j <= len (f ^ (mid g,2,(len g))) by A85, NAT_D:46;

A96: now

assume 1 > j -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1)
then (j -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then A97: j -' (len f) = 0 by XREAL_1:8;
then j - (len f) = 0 by A85, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1) by A1, A61, A97, FINSEQ_1:85; :: thesis: verum

end;

1 <= j + 1 by A90, NAT_D:48;
then A98: (f ^ (mid g,2,(len g))) /. (j + 1) = (f ^ (mid g,2,(len g))) . (j + 1) by A85, FINSEQ_4:24;
A99: LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f ^ (mid g,2,(len g))),i by A87, A91, TOPREAL1:def 5;
A100: 1 <= i + 1 by A91, NAT_D:48;
then A101: f /. (i + 1) = f . (i + 1) by A85, FINSEQ_4:24;

A102: now

assume 1 > (j + 1) -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1)
then ((j + 1) -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then A103: (j + 1) -' (len f) = 0 by XREAL_1:8;
then (j + 1) - (len f) = 0 by A88, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) by A1, A61, A103, FINSEQ_1:85; :: thesis: verum

end;

(j + 1) + 1 <= ((len f) + ((len g) - 1)) + 1 by A6, A10, A85, XREAL_1:8;
then ((j + 1) + 1) - (len f) <= ((len f) + (len g)) - (len f) by XREAL_1:11;
then ((j - (len f)) + 1) + 1 <= len g ;
then A104: ((j -' (len f)) + 1) + 1 <= len g by A86, XREAL_1:235;
then (j -' (len f)) + 1 <= len g by NAT_D:46;
then A105: g /. ((j -' (len f)) + 1) = g . ((j -' (len f)) + 1) by FINSEQ_4:24, NAT_1:11;
(((j -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by A104, XREAL_1:11;
then A106: (j -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then (j -' (len f)) + 1 <= ((len g) -' 2) + 1 by A8, XREAL_1:235;
then A107: j -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;

A108: now

assume A109: 1 <= j -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1)
then 1 <= j - (len f) by NAT_D:39;
then 1 + (len f) <= (j - (len f)) + (len f) by XREAL_1:8;
then A110: len f < j by NAT_1:13;
then (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j - (len f)) by A95, Th15;
then (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j -' (len f)) by A110, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . j = g . (((j -' (len f)) + 2) - 1) by A8, A107, A109, Th31;
hence (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1) ; :: thesis: verum

end;

A111: (j -' (len f)) + 1 = (j - (len f)) + 1 by A85, XREAL_1:235
.= (j + 1) - (len f)
.= (j + 1) -' (len f) by A88, XREAL_1:235 ;

A112: now

assume A113: 1 <= (j + 1) -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1)
then 1 <= (j + 1) - (len f) by NAT_D:39;
then 1 + (len f) <= ((j + 1) - (len f)) + (len f) by XREAL_1:8;
then A114: len f < j + 1 by NAT_1:13;
then (f ^ (mid g,2,(len g))) . (j + 1) = (mid g,2,(len g)) . ((j + 1) - (len f)) by A85, Th15;
then (f ^ (mid g,2,(len g))) . (j + 1) = (mid g,2,(len g)) . ((j + 1) -' (len f)) by A114, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . (j + 1) = g . ((((j + 1) -' (len f)) + 2) - 1) by A8, A106, A111, A113, Th31;
hence (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) ; :: thesis: verum

end;

1 <= 1 + (j -' (len f)) by NAT_1:11;
then A115: LSeg g,((j -' (len f)) + 1) = LSeg (g /. ((j -' (len f)) + 1)),(g /. (((j -' (len f)) + 1) + 1)) by A104, TOPREAL1:def 5;
1 <= j by A89, NAT_D:46;
then A116: (f ^ (mid g,2,(len g))) /. j = g /. ((j -' (len f)) + 1) by A95, A105, A108, A96, FINSEQ_4:24;
g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by A104, FINSEQ_4:24, NAT_1:11;
then LSeg (f ^ (mid g,2,(len g))),j = LSeg g,((j -' (len f)) + 1) by A85, A90, A111, A115, A116, A98, A112, A102, TOPREAL1:def 5;
then A117: LSeg (f ^ (mid g,2,(len g))),j c= L~ g by TOPREAL3:26;
A118: (i + 1) + 1 <= len f by A86, NAT_1:13;
(f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A87, A100, FINSEQ_4:24;
then LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f /. i),(f /. (i + 1)) by A85, A100, A94, A101, FINSEQ_1:85;
then A119: LSeg (f ^ (mid g,2,(len g))),i = LSeg f,i by A85, A91, A99, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),i c= L~ f by TOPREAL3:26;
then A120: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) c= {(g . 1)} by A4, A117, XBOOLE_1:27;

now

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

case A121: i + 1 < (len f) -' 1 ; :: thesis: LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j

A122: 1 <= len f by A5, XXREAL_0:2;
A123: ((len f) -' 1) + 1 = ((len f) - 1) + 1 by A5, XREAL_1:235, XXREAL_0:2
.= len f ;
A124: (1 + 1) - 1 <= (len f) - 1 by A5, XREAL_1:11;

now

f /. (len f) in LSeg f,((len f) -' 1) by A124, A123, TOPREAL1:27;
then A125: g . 1 in LSeg f,((len f) -' 1) by A1, A122, FINSEQ_4:24;
given x being set such that A126: x in (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) ; :: thesis: contradiction
A127: x in LSeg f,i by A119, A126, XBOOLE_0:def 4;
x = g . 1 by A120, A126, TARSKI:def 1;
then x in (LSeg f,i) /\ (LSeg f,((len f) -' 1)) by A127, A125, XBOOLE_0:def 4;
then LSeg f,i meets LSeg f,((len f) -' 1) by XBOOLE_0:4;
hence contradiction by A2, A121, TOPREAL1:def 9; :: thesis: verum

end;

hence LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j by XBOOLE_0:4; :: thesis: verum

end;

case i + 1 >= (len f) -' 1 ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

then i + 1 >= (len f) - 1 by A5, XREAL_1:235, XXREAL_0:2;
then A128: (i + 1) + 1 >= ((len f) - 1) + 1 by XREAL_1:8;
then A129: (i + 1) + 1 = len f by A118, XXREAL_0:1;
then A130: i + 1 <= len f by NAT_1:11;
i + 1 = (len f) - 1 by A129;
then A131: i + 1 = (len f) -' 1 by A5, XREAL_1:235, XXREAL_0:2;
A132: ((len f) -' 1) + 1 = ((len f) - 1) + 1 by A5, XREAL_1:235, XXREAL_0:2
.= len f ;
then 1 + 1 <= ((len f) -' 1) + 1 by A2, TOPREAL1:def 10;
then A133: 1 <= (len f) -' 1 by XREAL_1:8;
A134: i + (1 + 1) = len f by A118, A128, XXREAL_0:1;

now

(1 + 1) - 1 <= (len f) - 1 by A5, XREAL_1:11;
then A135: 1 <= (len f) -' 1 by NAT_D:39;
(len f) -' 1 <= len f by NAT_D:35;
then A136: (len f) -' 1 in dom f by A135, FINSEQ_3:27;
A137: (LSeg f,i) /\ (LSeg f,((len f) -' 1)) = {(f /. (i + 1))} by A2, A91, A131, A134, TOPREAL1:def 8;
f /. (len f) in LSeg f,((len f) -' 1) by A132, A133, TOPREAL1:27;
then A138: g . 1 in LSeg f,((len f) -' 1) by A1, A61, FINSEQ_4:24;
given x being set such that A139: x in (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) ; :: thesis: contradiction
A140: x = g . 1 by A120, A139, TARSKI:def 1;
x in LSeg f,i by A119, A139, XBOOLE_0:def 4;
then x in (LSeg f,i) /\ (LSeg f,((len f) -' 1)) by A140, A138, XBOOLE_0:def 4;
then f . (len f) = f /. (i + 1) by A1, A140, A137, TARSKI:def 1;
then A141: f . (len f) = f . ((len f) -' 1) by A131, A130, FINSEQ_4:24, NAT_1:11;
len f in dom f by A61, FINSEQ_3:27;
then len f = (len f) -' 1 by A2, A141, A136, FUNCT_1:def 8;
then len f = (len f) - 1 by A5, XREAL_1:235, XXREAL_0:2;
hence contradiction ; :: thesis: verum

end;

hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} by XBOOLE_0:def 1; :: thesis: verum

end;

end;

end;

hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} by XBOOLE_0:def 7; :: thesis: verum

end;

case i < 1 ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

then LSeg (f ^ (mid g,2,(len g))),i = {} by TOPREAL1:def 5;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} ; :: thesis: verum

end;

case A142: ( i + 1 <= len f & len f < j ) ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

(1 + 1) - 1 <= (len g) - 1 by A8, XREAL_1:11;
then (len f) + 1 <= (len f) + (len (mid g,2,(len g))) by A10, XREAL_1:9;
then len f < (len f) + (len (mid g,2,(len g))) by NAT_1:13;
then A143: i + 1 < len (f ^ (mid g,2,(len g))) by A6, A142, XXREAL_0:2;
A144: len f <= j + 1 by A142, NAT_D:48;
A145: 1 + 1 <= j by A5, A142, XXREAL_0:2;
then A146: 1 <= j by NAT_D:46;

now

per cases ( 1 <= i or i < 1 ) ;

case A147: 1 <= i ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

i <= len f by A85, NAT_D:46;
then A148: f /. i = f . i by A147, FINSEQ_4:24;
i <= len (f ^ (mid g,2,(len g))) by A143, NAT_D:46;
then A149: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A147, FINSEQ_4:24;
i <= len f by A85, NAT_D:46;
then A150: (f ^ (mid g,2,(len g))) /. i = f /. i by A147, A149, A148, FINSEQ_1:85;
A151: LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f ^ (mid g,2,(len g))),i by A143, A147, TOPREAL1:def 5;
A152: 1 <= i + 1 by A147, NAT_D:48;
then A153: f /. (i + 1) = f . (i + 1) by A85, FINSEQ_4:24;
(f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A143, A152, FINSEQ_4:24;
then LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f /. i),(f /. (i + 1)) by A85, A152, A150, A153, FINSEQ_1:85;
then LSeg (f ^ (mid g,2,(len g))),i = LSeg f,i by A85, A147, A151, TOPREAL1:def 5;
then A154: LSeg (f ^ (mid g,2,(len g))),i c= L~ f by TOPREAL3:26;
A155: j <= len (f ^ (mid g,2,(len g))) by A85, NAT_D:46;

A156: now

assume 1 > j -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1)
then (j -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then A157: j -' (len f) = 0 by XREAL_1:8;
then j - (len f) = 0 by A85, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1) by A1, A61, A157, FINSEQ_1:85; :: thesis: verum

end;

1 <= j + 1 by A146, NAT_D:48;
then A158: (f ^ (mid g,2,(len g))) /. (j + 1) = (f ^ (mid g,2,(len g))) . (j + 1) by A85, FINSEQ_4:24;

A159: now

assume 1 > (j + 1) -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1)
then ((j + 1) -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then A160: (j + 1) -' (len f) = 0 by XREAL_1:8;
then (j + 1) - (len f) = 0 by A144, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) by A1, A61, A160, FINSEQ_1:85; :: thesis: verum

end;

(j + 1) + 1 <= ((len f) + ((len g) - 1)) + 1 by A6, A10, A85, XREAL_1:8;
then ((j + 1) + 1) - (len f) <= ((len f) + (len g)) - (len f) by XREAL_1:11;
then ((j - (len f)) + 1) + 1 <= len g ;
then A161: ((j -' (len f)) + 1) + 1 <= len g by A142, XREAL_1:235;
then (j -' (len f)) + 1 <= len g by NAT_D:46;
then A162: g /. ((j -' (len f)) + 1) = g . ((j -' (len f)) + 1) by FINSEQ_4:24, NAT_1:11;
(((j -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by A161, XREAL_1:11;
then A163: (j -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then (j -' (len f)) + 1 <= ((len g) -' 2) + 1 by A8, XREAL_1:235;
then A164: j -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;

A165: now

assume A166: 1 <= j -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1)
then 1 <= j - (len f) by NAT_D:39;
then 1 + (len f) <= (j - (len f)) + (len f) by XREAL_1:8;
then A167: len f < j by NAT_1:13;
then (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j - (len f)) by A155, Th15;
then (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j -' (len f)) by A167, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . j = g . (((j -' (len f)) + 2) - 1) by A8, A164, A166, Th31;
hence (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1) ; :: thesis: verum

end;

A168: (j -' (len f)) + 1 = (j - (len f)) + 1 by A85, XREAL_1:235
.= (j + 1) - (len f)
.= (j + 1) -' (len f) by A144, XREAL_1:235 ;

A169: now

assume A170: 1 <= (j + 1) -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1)
then 1 <= (j + 1) - (len f) by NAT_D:39;
then 1 + (len f) <= ((j + 1) - (len f)) + (len f) by XREAL_1:8;
then A171: len f < j + 1 by NAT_1:13;
then (f ^ (mid g,2,(len g))) . (j + 1) = (mid g,2,(len g)) . ((j + 1) - (len f)) by A85, Th15;
then (f ^ (mid g,2,(len g))) . (j + 1) = (mid g,2,(len g)) . ((j + 1) -' (len f)) by A171, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . (j + 1) = g . ((((j + 1) -' (len f)) + 2) - 1) by A8, A163, A168, A170, Th31;
hence (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) ; :: thesis: verum

end;

1 <= 1 + (j -' (len f)) by NAT_1:11;
then A172: LSeg g,((j -' (len f)) + 1) = LSeg (g /. ((j -' (len f)) + 1)),(g /. (((j -' (len f)) + 1) + 1)) by A161, TOPREAL1:def 5;
1 <= j by A145, NAT_D:46;
then A173: (f ^ (mid g,2,(len g))) /. j = g /. ((j -' (len f)) + 1) by A155, A162, A165, A156, FINSEQ_4:24;
g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by A161, FINSEQ_4:24, NAT_1:11;
then A174: LSeg (f ^ (mid g,2,(len g))),j = LSeg g,((j -' (len f)) + 1) by A85, A146, A168, A172, A173, A158, A169, A159, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),j c= L~ g by TOPREAL3:26;
then A175: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) c= {(g . 1)} by A4, A154, XBOOLE_1:27;

now

A176: 1 + 1 in dom g by A8, FINSEQ_3:27;
A177: (j -' (len f)) + 1 = (j - (len f)) + 1 by A142, XREAL_1:235;
A178: 1 + 1 <= len g by A3, TOPREAL1:def 10;
given x being set such that A179: x in (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) ; :: thesis: contradiction
A180: x in LSeg g,((j -' (len f)) + 1) by A174, A179, XBOOLE_0:def 4;
A181: x = g . 1 by A175, A179, TARSKI:def 1;
then g /. 1 = x by A9, FINSEQ_4:24;
then x in LSeg g,1 by A178, TOPREAL1:27;
then A182: x in (LSeg g,1) /\ (LSeg g,((j -' (len f)) + 1)) by A180, XBOOLE_0:def 4;
then LSeg g,1 meets LSeg g,((j -' (len f)) + 1) by XBOOLE_0:4;
then 1 + 1 >= (j -' (len f)) + 1 by A3, TOPREAL1:def 9;
then 1 >= j -' (len f) by XREAL_1:8;
then 1 >= j - (len f) by NAT_D:39;
then A183: 1 + (len f) >= (j - (len f)) + (len f) by XREAL_1:8;
j >= (len f) + 1 by A142, NAT_1:13;
then A184: j = (len f) + 1 by A183, XXREAL_0:1;
LSeg g,((j -' (len f)) + 1) <> {} by A174, A179;
then 1 + 2 <= len g by A184, A177, TOPREAL1:def 5;
then (LSeg g,1) /\ (LSeg g,((j -' (len f)) + 1)) = {(g /. (1 + 1))} by A3, A184, A177, TOPREAL1:def 8;
then A185: x = g /. (1 + 1) by A182, TARSKI:def 1
.= g . (1 + 1) by A8, FINSEQ_4:24 ;
1 in dom g by A9, FINSEQ_3:27;
hence contradiction by A3, A181, A185, A176, FUNCT_1:def 8; :: thesis: verum

end;

hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} by XBOOLE_0:def 1; :: thesis: verum

end;

case i < 1 ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

then LSeg (f ^ (mid g,2,(len g))),i = {} by TOPREAL1:def 5;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} ; :: thesis: verum

end;

end;

end;

hence LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j by XBOOLE_0:def 7; :: thesis: verum

end;

case A186: ( len f < i + 1 & j + 1 <= len (f ^ (mid g,2,(len g))) ) ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

then A187: len f <= i by NAT_1:13;
then A188: i -' (len f) = i - (len f) by XREAL_1:235;
A189: 1 + 1 <= i by A5, A187, XXREAL_0:2;
then A190: 1 <= i by NAT_D:46;
then A191: 1 <= i + 1 by NAT_D:48;
then A192: 1 <= j by A63, XXREAL_0:2;
A193: 1 <= (j -' (len f)) + 1 by NAT_1:11;
A194: len f < j by A63, A186, XXREAL_0:2;
j <= j + 1 by NAT_1:11;
then A195: len f < j + 1 by A194, XXREAL_0:2;
A196: 1 <= (i -' (len f)) + 1 by NAT_1:11;
A197: j -' (len f) = j - (len f) by A63, A186, XREAL_1:235, XXREAL_0:2;
(i + 1) - (len f) < j - (len f) by A63, XREAL_1:11;
then A198: ((i -' (len f)) + 1) + 1 < (j -' (len f)) + 1 by A188, A197, XREAL_1:8;

now

per cases ( j + 1 <= len (f ^ (mid g,2,(len g))) or j + 1 > len (f ^ (mid g,2,(len g))) ) ;

case A199: j + 1 <= len (f ^ (mid g,2,(len g))) ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

A200: 1 <= j by A63, A191, XXREAL_0:2;
then 1 <= j + 1 by NAT_D:48;
then A201: (f ^ (mid g,2,(len g))) /. (j + 1) = (f ^ (mid g,2,(len g))) . (j + 1) by A199, FINSEQ_4:24;
(len f) + 1 <= j by A194, NAT_1:13;
then A202: ((len f) + 1) - (len f) <= j - (len f) by XREAL_1:11;
A203: 1 <= i by A189, NAT_D:46;
then A204: 1 <= i + 1 by NAT_D:48;
A205: j <= len (f ^ (mid g,2,(len g))) by A199, NAT_D:46;
then A206: i + 1 < len (f ^ (mid g,2,(len g))) by A63, XXREAL_0:2;
then A207: i <= len (f ^ (mid g,2,(len g))) by NAT_D:46;
i + 1 < (len f) + ((len g) - 1) by A10, A206, FINSEQ_1:35;
then A208: (i + 1) - (len f) < ((len f) + ((len g) - 1)) - (len f) by XREAL_1:11;
then A209: ((i - (len f)) + 1) + 1 < ((len g) - 1) + 1 by XREAL_1:8;
then ((i -' (len f)) + 1) + 1 <= len g by A187, XREAL_1:235;
then A210: g /. (((i -' (len f)) + 1) + 1) = g . (((i -' (len f)) + 1) + 1) by FINSEQ_4:24, NAT_1:11;
i + 1 <= len (f ^ (mid g,2,(len g))) by A63, A205, XXREAL_0:2;
then A211: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A204, FINSEQ_4:24;
A212: LSeg ((f ^ (mid g,2,(len g))) /. j),((f ^ (mid g,2,(len g))) /. (j + 1)) = LSeg (f ^ (mid g,2,(len g))),j by A192, A199, TOPREAL1:def 5;
A213: LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f ^ (mid g,2,(len g))),i by A190, A206, TOPREAL1:def 5;
A214: (i -' (len f)) + 1 <= len g by A188, A209, NAT_D:46;
then A215: g /. ((i -' (len f)) + 1) = g . ((i -' (len f)) + 1) by FINSEQ_4:24, NAT_1:11;

A216: now

per cases ( i <= len f or i > len f ) ;

case i <= len f ; :: thesis: (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1)

then A217: i = len f by A187, XXREAL_0:1;
then (f ^ (mid g,2,(len g))) . i = g . (0 + 1) by A1, A190, FINSEQ_1:85
.= g . ((i -' (len f)) + 1) by A217, XREAL_1:234 ;
hence (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1) by A203, A207, A215, FINSEQ_4:24; :: thesis: verum

end;

case A218: i > len f ; :: thesis: (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1)

then (len f) + 1 <= i by NAT_1:13;
then A219: ((len f) + 1) - (len f) <= i - (len f) by XREAL_1:11;
((i -' (len f)) + 1) - 1 <= (len g) - 1 by A214, XREAL_1:11;
then A220: i -' (len f) <= ((len g) - 2) + 1 ;
(f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i -' (len f)) by A188, A207, A218, Th15
.= g . (((i -' (len f)) + 2) - 1) by A8, A188, A219, A220, Th31
.= g . ((i -' (len f)) + 1) ;
hence (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1) by A203, A207, A215, FINSEQ_4:24; :: thesis: verum

end;

end;

end;

j + 1 <= (len f) + ((len g) - 1) by A10, A199, FINSEQ_1:35;
then A221: (j + 1) - (len f) <= ((len f) + ((len g) - 1)) - (len f) by XREAL_1:11;
then A222: (j -' (len f)) + 1 <= ((len g) - 2) + 1 by A197;
A223: (((j -' (len f)) + 1) + 2) - 1 = ((j -' (len f)) + 1) + 1 ;
A224: (f ^ (mid g,2,(len g))) . (j + 1) = (mid g,2,(len g)) . ((j + 1) - (len f)) by A195, A199, Th15
.= g . (((j -' (len f)) + 1) + 1) by A8, A197, A193, A222, A223, Th31 ;
A225: (((i -' (len f)) + 1) + 2) - 1 = ((i -' (len f)) + 1) + 1 ;
A226: (i -' (len f)) + 1 <= ((len g) - 2) + 1 by A188, A208;
(f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) - (len f)) by A186, A206, Th15
.= g . (((i -' (len f)) + 1) + 1) by A8, A188, A196, A226, A225, Th31 ;
then A227: LSeg (f ^ (mid g,2,(len g))),i = LSeg g,((i -' (len f)) + 1) by A188, A196, A209, A216, A211, A210, A213, TOPREAL1:def 5;
A228: ((j - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by A221, XREAL_1:8;
then A229: (j -' (len f)) + 1 <= len g by A197, NAT_D:46;
then A230: g /. ((j -' (len f)) + 1) = g . ((j -' (len f)) + 1) by FINSEQ_4:24, NAT_1:11;
A231: j <= len (f ^ (mid g,2,(len g))) by A199, NAT_D:46;
then A232: (f ^ (mid g,2,(len g))) /. j = (f ^ (mid g,2,(len g))) . j by A200, FINSEQ_4:24;
((j -' (len f)) + 1) + 1 <= len g by A63, A186, A228, XREAL_1:235, XXREAL_0:2;
then A233: g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by FINSEQ_4:24, NAT_1:11;
((j -' (len f)) + 1) - 1 <= (len g) - 1 by A229, XREAL_1:11;
then A234: j -' (len f) <= ((len g) - 2) + 1 ;
(f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j - (len f)) by A194, A231, Th15
.= g . (((j -' (len f)) + 2) - 1) by A8, A197, A202, A234, Th31
.= g . ((j -' (len f)) + 1) ;
then LSeg (f ^ (mid g,2,(len g))),j = LSeg g,((j -' (len f)) + 1) by A197, A193, A228, A232, A230, A201, A233, A224, A212, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j by A3, A198, A227, TOPREAL1:def 9;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} by XBOOLE_0:def 7; :: thesis: verum

end;

case j + 1 > len (f ^ (mid g,2,(len g))) ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

then LSeg (f ^ (mid g,2,(len g))),j = {} by TOPREAL1:def 5;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} ; :: thesis: verum

end;

case j + 1 > len (f ^ (mid g,2,(len g))) ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {}

then LSeg (f ^ (mid g,2,(len g))),j = {} by TOPREAL1:def 5;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) = {} ; :: thesis: verum

end;

end;

end;

hence LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j by XBOOLE_0:def 7; :: thesis: verum

end;

A235: for i being Nat st 1 <= i & i + 2 <= len (f ^ (mid g,2,(len g))) holds
(LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))}

proof

let i be Nat; :: thesis: ( 1 <= i & i + 2 <= len (f ^ (mid g,2,(len g))) implies (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))} )
assume that
A236: 1 <= i and
A237: i + 2 <= len (f ^ (mid g,2,(len g))) ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))}
A238: 1 <= i + 1 by A236, NAT_D:48;
A239: i <= len (f ^ (mid g,2,(len g))) by A237, NAT_D:47;
A240: 1 <= (i + 1) + 1 by A236, NAT_D:48;
A241: i + 1 <= len (f ^ (mid g,2,(len g))) by A237, NAT_D:47;
(i + 1) + 1 <= (len f) + (len (mid g,2,(len g))) by A237, FINSEQ_1:35;
then (i + 1) + 1 <= (len f) + (((len g) -' 2) + 1) by A8, A9, Th27;
then (i + 1) + 1 <= (len f) + (((len g) - (1 + 1)) + 1) by A8, XREAL_1:235;
then A242: ((i + 1) + 1) - (len f) <= ((len f) + (((len g) - (1 + 1)) + 1)) - (len f) by XREAL_1:11;
then A243: (((i + 1) - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by XREAL_1:8;
then A244: (((i - (len f)) + 1) + 1) + 1 <= len g ;

now

per cases ( i + 2 <= len f or i + 2 > len f ) ;

case A245: i + 2 <= len f ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))}

A246: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A238, A241, FINSEQ_4:24;
(i + 1) + 1 <= len f by A245;
then A247: i + 1 <= len f by NAT_D:46;
then f /. (i + 1) = f . (i + 1) by A238, FINSEQ_4:24;
then A248: (f ^ (mid g,2,(len g))) /. (i + 1) = f /. (i + 1) by A238, A247, A246, FINSEQ_1:85;
A249: f /. ((i + 1) + 1) = f . ((i + 1) + 1) by A240, A245, FINSEQ_4:24;
A250: LSeg ((f ^ (mid g,2,(len g))) /. (i + 1)),((f ^ (mid g,2,(len g))) /. ((i + 1) + 1)) = LSeg (f ^ (mid g,2,(len g))),(i + 1) by A237, A238, TOPREAL1:def 5;
A251: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A236, A239, FINSEQ_4:24;
A252: i <= len f by A247, NAT_D:46;
then f /. i = f . i by A236, FINSEQ_4:24;
then A253: (f ^ (mid g,2,(len g))) /. i = f /. i by A236, A252, A251, FINSEQ_1:85;
(f ^ (mid g,2,(len g))) /. ((i + 1) + 1) = (f ^ (mid g,2,(len g))) . ((i + 1) + 1) by A237, A240, FINSEQ_4:24;
then LSeg ((f ^ (mid g,2,(len g))) /. (i + 1)),((f ^ (mid g,2,(len g))) /. ((i + 1) + 1)) = LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) by A240, A245, A248, A249, FINSEQ_1:85;
then A254: LSeg (f ^ (mid g,2,(len g))),(i + 1) = LSeg f,(i + 1) by A238, A245, A250, TOPREAL1:def 5;
LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f ^ (mid g,2,(len g))),i by A236, A241, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),i = LSeg f,i by A236, A247, A253, A248, TOPREAL1:def 5;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))} by A2, A236, A245, A248, A254, TOPREAL1:def 8; :: thesis: verum

end;

case i + 2 > len f ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))}

then A255: i + 2 >= (len f) + 1 by NAT_1:13;

now

per cases ( i + 2 > (len f) + 1 or i + 2 = (len f) + 1 ) by A255, XXREAL_0:1;

case A256: i + 2 > (len f) + 1 ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))}

then (i + 1) + 1 > (len f) + 1 ;
then A257: i + 1 >= (len f) + 1 by NAT_1:13;
then A258: i >= len f by XREAL_1:8;

A259: now

assume 1 > i -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1)
then (i -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then A260: i -' (len f) = 0 by XREAL_1:8;
then i - (len f) = 0 by A258, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1) by A1, A61, A260, FINSEQ_1:85; :: thesis: verum

end;

A261: i + 1 >= len f by A257, NAT_D:48;

A262: now

assume 1 > (i + 1) -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . (i + 1) = g . (((i + 1) -' (len f)) + 1)
then ((i + 1) -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then A263: (i + 1) -' (len f) = 0 by XREAL_1:8;
then (i + 1) - (len f) = 0 by A261, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . (i + 1) = g . (((i + 1) -' (len f)) + 1) by A1, A61, A263, FINSEQ_1:85; :: thesis: verum

end;

(i + 1) + 1 >= ((len f) + 1) + 1 by A256, NAT_1:13;
then ((i + 1) + 1) - ((len f) + 1) >= (((len f) + 1) + 1) - ((len f) + 1) by XREAL_1:11;
then (i - (len f)) + 1 >= 1 ;
then A264: (i -' (len f)) + 1 >= 1 by A258, XREAL_1:235;
then A265: ((i -' (len f)) + 1) + 1 >= 1 by NAT_D:48;
then A266: ((i - (len f)) + 1) + 1 >= 1 by A258, XREAL_1:235;
then ((i + 1) - (len f)) + 1 >= 1 ;
then A267: ((i + 1) -' (len f)) + 1 >= 1 by A261, XREAL_1:235;
then A268: (((i + 1) -' (len f)) + 1) + 1 >= 1 by NAT_D:48;
((i + 1) - (len f)) + 1 >= 0 + 1 by A266;
then A269: (i + 1) - (len f) >= 0 by XREAL_1:8;
then (((i + 1) -' (len f)) + 1) + 1 <= len g by A243, XREAL_0:def 2;
then A270: g /. ((((i + 1) -' (len f)) + 1) + 1) = g . ((((i + 1) -' (len f)) + 1) + 1) by A268, FINSEQ_4:24;
(((i + 1) -' (len f)) + 1) + 1 <= len g by A243, A261, XREAL_1:235;
then A271: LSeg g,(((i + 1) -' (len f)) + 1) = LSeg (g /. (((i + 1) -' (len f)) + 1)),(g /. ((((i + 1) -' (len f)) + 1) + 1)) by A267, TOPREAL1:def 5;
(((i + 1) + 1) - (len f)) + 1 = (((i + 1) - (len f)) + 1) + 1 ;
then A272: (((i + 1) + 1) - (len f)) + 1 = (((i + 1) -' (len f)) + 1) + 1 by A269, XREAL_0:def 2;
A273: (((i -' (len f)) + 1) + 1) + 1 <= len g by A244, A258, XREAL_1:235;
then A274: ((i -' (len f)) + 1) + 1 <= len g by NAT_D:46;
then A275: LSeg g,((i -' (len f)) + 1) = LSeg (g /. ((i -' (len f)) + 1)),(g /. (((i -' (len f)) + 1) + 1)) by A264, TOPREAL1:def 5;
(((i -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by A274, XREAL_1:11;
then (i -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then A276: (i -' (len f)) + 1 <= ((len g) -' 2) + 1 by A8, XREAL_1:235;
then A277: i -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;

A278: now

assume A279: 1 <= i -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1)
then 1 <= i - (len f) by NAT_D:39;
then 1 + (len f) <= (i - (len f)) + (len f) by XREAL_1:8;
then A280: len f < i by NAT_1:13;
then (f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i - (len f)) by A239, Th15;
then (f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i -' (len f)) by A280, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . i = g . (((i -' (len f)) + 2) - 1) by A8, A277, A279, Th31;
hence (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1) ; :: thesis: verum

end;

(i -' (len f)) + 1 <= len g by A274, NAT_D:46;
then g /. ((i -' (len f)) + 1) = g . ((i -' (len f)) + 1) by A264, FINSEQ_4:24;
then A281: (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1) by A236, A239, A278, A259, FINSEQ_4:24;
A282: ((i -' (len f)) + 1) + (1 + 1) <= len g by A273;
A283: g /. (((i -' (len f)) + 1) + 1) = g . (((i -' (len f)) + 1) + 1) by A274, A265, FINSEQ_4:24;
(i - (len f)) + 1 <= ((len g) -' 2) + 1 by A258, A276, XREAL_1:235;
then (i + 1) - (len f) <= ((len g) -' 2) + 1 ;
then A284: (i + 1) -' (len f) <= ((len g) -' 2) + 1 by A261, XREAL_1:235;

A285: now

assume A286: 1 <= (i + 1) -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . (i + 1) = g . (((i + 1) -' (len f)) + 1)
then 1 <= (i + 1) - (len f) by NAT_D:39;
then 1 + (len f) <= ((i + 1) - (len f)) + (len f) by XREAL_1:8;
then A287: len f < i + 1 by NAT_1:13;
then (f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) - (len f)) by A241, Th15;
then (f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) -' (len f)) by A287, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . (i + 1) = g . ((((i + 1) -' (len f)) + 2) - 1) by A8, A284, A286, Th31;
hence (f ^ (mid g,2,(len g))) . (i + 1) = g . (((i + 1) -' (len f)) + 1) ; :: thesis: verum

end;

A288: now

assume 1 > ((i + 1) + 1) -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1)
then A289: (((i + 1) + 1) -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then ((i + 1) + 1) -' (len f) <= 0 by XREAL_1:8;
then A290: ((i + 1) + 1) - (len f) = 0 by A266, XREAL_0:def 2;
((i + 1) + 1) -' (len f) = 0 by A289, XREAL_1:8;
hence (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1) by A1, A61, A290, FINSEQ_1:85; :: thesis: verum

end;

((i + 1) - (len f)) + 1 = ((i - (len f)) + 1) + 1 ;
then A291: ((i + 1) - (len f)) + 1 = ((i -' (len f)) + 1) + 1 by A258, XREAL_1:235;
then A292: ((i + 1) -' (len f)) + 1 = ((i -' (len f)) + 1) + 1 by A261, XREAL_1:235;
A293: ((i + 1) + 1) -' (len f) <= ((len g) - 2) + 1 by A242, A266, XREAL_0:def 2;

A294: now

assume A295: 1 <= ((i + 1) + 1) -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1)
then 1 <= ((i + 1) + 1) - (len f) by NAT_D:39;
then 1 + (len f) <= (((i + 1) + 1) - (len f)) + (len f) by XREAL_1:8;
then A296: len f < (i + 1) + 1 by NAT_1:13;
then (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = (mid g,2,(len g)) . (((i + 1) + 1) - (len f)) by A237, Th15;
then (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = (mid g,2,(len g)) . (((i + 1) + 1) -' (len f)) by A296, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . (((((i + 1) + 1) -' (len f)) + 2) - 1) by A8, A293, A295, Th31;
hence (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1) ; :: thesis: verum

end;

A297: (f ^ (mid g,2,(len g))) /. ((i + 1) + 1) = (f ^ (mid g,2,(len g))) . ((i + 1) + 1) by A237, A240, FINSEQ_4:24;
A298: LSeg (f ^ (mid g,2,(len g))),i = LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) by A236, A241, TOPREAL1:def 5;
A299: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A238, A241, FINSEQ_4:24;
LSeg (f ^ (mid g,2,(len g))),(i + 1) = LSeg ((f ^ (mid g,2,(len g))) /. (i + 1)),((f ^ (mid g,2,(len g))) /. ((i + 1) + 1)) by A237, A238, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),(i + 1) = LSeg g,(((i + 1) -' (len f)) + 1) by A291, A272, A299, A283, A285, A262, A271, A297, A270, A294, A288, XREAL_0:def 2;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))} by A3, A264, A292, A298, A275, A281, A299, A283, A285, A282, TOPREAL1:def 8; :: thesis: verum

end;

case A300: i + 2 = (len f) + 1 ; :: thesis: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))}

then A301: f /. (i + 1) = f . (i + 1) by A238, FINSEQ_4:24;
then A302: f /. (i + 1) = g /. 1 by A1, A9, A300, FINSEQ_4:24;
(f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A238, A241, FINSEQ_4:24;
then A303: (f ^ (mid g,2,(len g))) /. (i + 1) = f /. (i + 1) by A238, A300, A301, FINSEQ_1:85;
A304: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A236, A300, TOPREAL1:def 5;
A305: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A236, A239, FINSEQ_4:24;
(i + 1) + 1 = (len f) + 1 by A300;
then A306: i <= len f by NAT_D:46;
then f /. i = f . i by A236, FINSEQ_4:24;
then A307: (f ^ (mid g,2,(len g))) /. i = f /. i by A236, A306, A305, FINSEQ_1:85;
A308: LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f ^ (mid g,2,(len g))),i by A236, A241, TOPREAL1:def 5;
i = (len f) - 1 by A300;
then A309: i = (len f) -' 1 by A5, XREAL_1:235, XXREAL_0:2;
A310: g /. 1 in LSeg (g /. 1),(g /. (1 + 1)) by RLTOPSP1:69;
A311: g /. 1 = g . 1 by A9, FINSEQ_4:24;
then g /. 1 = f /. (len f) by A1, A61, FINSEQ_4:24;
then A312: g /. 1 in LSeg (f /. ((len f) -' 1)),(f /. (len f)) by RLTOPSP1:69;
(len g) - 2 >= 0 by A8, XREAL_1:50;
then A313: 0 + 1 <= ((len g) - 2) + 1 by XREAL_1:8;
len f < (i + 1) + 1 by A300, NAT_1:13;
then (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = (mid g,2,(len g)) . (((i + 1) + 1) - (len f)) by A237, Th15;
then A314: (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . ((2 + 1) -' 1) by A8, A300, A313, Th31
.= g . 2 by NAT_D:34 ;
A315: LSeg g,1 c= L~ g by TOPREAL3:26;
LSeg f,i c= L~ f by TOPREAL3:26;
then A316: (LSeg f,i) /\ (LSeg g,1) c= {(g /. 1)} by A4, A311, A315, XBOOLE_1:27;
A317: ((i + 1) -' (len f)) + 1 = 0 + 1 by A300, XREAL_1:234
.= 1 ;
then A318: g /. ((((i + 1) -' (len f)) + 1) + 1) = g . ((((i + 1) -' (len f)) + 1) + 1) by A8, FINSEQ_4:24;
LSeg g,1 = LSeg (g /. 1),(g /. (1 + 1)) by A8, TOPREAL1:def 5;
then g /. 1 in (LSeg f,i) /\ (LSeg g,1) by A300, A309, A304, A312, A310, XBOOLE_0:def 4;
then A319: {(g /. 1)} c= (LSeg f,i) /\ (LSeg g,1) by ZFMISC_1:37;
A320: (f ^ (mid g,2,(len g))) /. ((i + 1) + 1) = (f ^ (mid g,2,(len g))) . ((i + 1) + 1) by A237, A240, FINSEQ_4:24;
A321: LSeg (f ^ (mid g,2,(len g))),(i + 1) = LSeg ((f ^ (mid g,2,(len g))) /. (i + 1)),((f ^ (mid g,2,(len g))) /. ((i + 1) + 1)) by A237, A238, TOPREAL1:def 5;
LSeg g,(((i + 1) -' (len f)) + 1) = LSeg (g /. (((i + 1) -' (len f)) + 1)),(g /. ((((i + 1) -' (len f)) + 1) + 1)) by A8, A317, TOPREAL1:def 5;
hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))} by A307, A302, A303, A308, A304, A321, A317, A320, A318, A314, A319, A316, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))} ; :: thesis: verum

end;

end;

end;

hence (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),(i + 1)) = {((f ^ (mid g,2,(len g))) /. (i + 1))} ; :: thesis: verum

end;

for i being Nat st 1 <= i & i + 1 <= len (f ^ (mid g,2,(len g))) & not ((f ^ (mid g,2,(len g))) /. i) `1 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `1 holds
((f ^ (mid g,2,(len g))) /. i) `2 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `2

proof

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len (f ^ (mid g,2,(len g))) & not ((f ^ (mid g,2,(len g))) /. i) `1 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `1 implies ((f ^ (mid g,2,(len g))) /. i) `2 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `2 )
assume that
A322: 1 <= i and
A323: i + 1 <= len (f ^ (mid g,2,(len g))) ; :: thesis: ( ((f ^ (mid g,2,(len g))) /. i) `1 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `1 or ((f ^ (mid g,2,(len g))) /. i) `2 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `2 )

now

per cases ( i < len f or i >= len f ) ;

case A324: i < len f ; :: thesis: ( ((f ^ (mid g,2,(len g))) /. i) `1 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `1 or ((f ^ (mid g,2,(len g))) /. i) `2 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `2 )

i <= len (f ^ (mid g,2,(len g))) by A323, NAT_D:46;
then A325: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A322, FINSEQ_4:24;
f /. i = f . i by A322, A324, FINSEQ_4:24;
then A326: (f ^ (mid g,2,(len g))) /. i = f /. i by A322, A324, A325, FINSEQ_1:85;
A327: 1 <= i + 1 by A322, NAT_D:48;
then A328: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A323, FINSEQ_4:24;
A329: i + 1 <= len f by A324, NAT_1:13;
then A330: (f ^ (mid g,2,(len g))) . (i + 1) = f . (i + 1) by A327, FINSEQ_1:85;
f /. (i + 1) = f . (i + 1) by A327, A329, FINSEQ_4:24;
hence ( ((f ^ (mid g,2,(len g))) /. i) `1 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `1 or ((f ^ (mid g,2,(len g))) /. i) `2 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `2 ) by A2, A322, A329, A326, A328, A330, TOPREAL1:def 7; :: thesis: verum

end;

case A331: i >= len f ; :: thesis: ( ((f ^ (mid g,2,(len g))) /. i) `1 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `1 or ((f ^ (mid g,2,(len g))) /. i) `2 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `2 )

1 <= 1 + (i -' (len f)) by NAT_1:11;
then 1 <= 1 + (i - (len f)) by A331, XREAL_1:235;
then 1 <= (1 + i) - (len f) ;
then A332: 1 <= (i + 1) -' (len f) by NAT_D:39;
A333: i <= len (f ^ (mid g,2,(len g))) by A323, NAT_D:46;
A334: i - (len f) >= 0 by A331, XREAL_1:50;
then A335: i -' (len f) = i - (len f) by XREAL_0:def 2;

A336: now

assume 1 > i -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1)
then (i -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then i -' (len f) = 0 by XREAL_1:8;
hence (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1) by A1, A61, A335, FINSEQ_1:85; :: thesis: verum

end;

A337: i + 1 >= len f by A331, NAT_D:48;
then A338: ((i + 1) -' (len f)) + 1 = ((i + 1) - (len f)) + 1 by XREAL_1:235
.= ((i - (len f)) + 1) + 1
.= ((i -' (len f)) + 1) + 1 by A331, XREAL_1:235 ;
A339: (i + 1) - (len f) <= ((len f) + ((len g) - 1)) - (len f) by A6, A10, A323, XREAL_1:11;
then A340: ((i - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by XREAL_1:8;
then A341: ((i -' (len f)) + 1) + 1 <= len g by A334, XREAL_0:def 2;
i -' (len f) <= (i -' (len f)) + 1 by NAT_1:11;
then A342: i -' (len f) <= ((len g) - 2) + 1 by A335, A339, XXREAL_0:2;

A343: now

assume A344: 1 <= i -' (len f) ; :: thesis: (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1)
then 1 <= i - (len f) by NAT_D:39;
then 1 + (len f) <= (i - (len f)) + (len f) by XREAL_1:8;
then A345: len f < i by NAT_1:13;
then (f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i - (len f)) by A333, Th15;
then (f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i -' (len f)) by A345, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . i = g . (((i -' (len f)) + 2) - 1) by A8, A342, A344, Th31;
hence (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1) ; :: thesis: verum

end;

1 <= i + 1 by A322, NAT_D:48;
then A346: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A323, FINSEQ_4:24;
A347: 1 <= (i -' (len f)) + 1 by NAT_1:11;
(i + 1) - (len f) <= ((len g) - 2) + 1 by A339;
then (i + 1) - (len f) <= ((len g) -' 2) + 1 by A8, XREAL_1:235;
then A348: (i + 1) -' (len f) <= ((len g) -' 2) + 1 by A337, XREAL_1:235;
len f < i + 1 by A331, NAT_1:13;
then (f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) - (len f)) by A323, Th15;
then (f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) -' (len f)) by A337, XREAL_1:235;
then A349: (f ^ (mid g,2,(len g))) . (i + 1) = g . ((((i + 1) -' (len f)) + 2) - 1) by A8, A348, A332, Th31;
((i -' (len f)) + 1) + 1 <= len g by A334, A340, XREAL_0:def 2;
then A350: g /. (((i -' (len f)) + 1) + 1) = g . (((i -' (len f)) + 1) + 1) by FINSEQ_4:24, NAT_1:11;
(i -' (len f)) + 1 <= len g by A335, A340, NAT_D:46;
then g /. ((i -' (len f)) + 1) = g . ((i -' (len f)) + 1) by FINSEQ_4:24, NAT_1:11;
then (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1) by A322, A333, A343, A336, FINSEQ_4:24;
hence ( ((f ^ (mid g,2,(len g))) /. i) `1 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `1 or ((f ^ (mid g,2,(len g))) /. i) `2 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `2 ) by A3, A347, A341, A338, A346, A350, A349, TOPREAL1:def 7; :: thesis: verum

end;

end;

end;

hence ( ((f ^ (mid g,2,(len g))) /. i) `1 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `1 or ((f ^ (mid g,2,(len g))) /. i) `2 = ((f ^ (mid g,2,(len g))) /. (i + 1)) `2 ) ; :: thesis: verum

end;

then ( f ^ (mid g,2,(len g)) is unfolded & f ^ (mid g,2,(len g)) is s.n.c. & f ^ (mid g,2,(len g)) is special ) by A235, A62, TOPREAL1:def 7, TOPREAL1:def 8, TOPREAL1:def 9;
hence f ^ (mid g,2,(len g)) is being_S-Seq by A60, A7, TOPREAL1:def 10; :: thesis: verum