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 A1: ( f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} ) ; :: thesis: f ^ (mid g,2,(len g)) is being_S-Seq
then A2: ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) by TOPREAL1:def 10;
A3: ( g is one-to-one & len g >= 2 & g is unfolded & g is s.n.c. & g is special ) by A1, TOPREAL1:def 10;
A4: 1 <= len f by A2, XXREAL_0:2;
A5: 1 <= len g by A3, XXREAL_0:2;
A6: len (f ^ (mid g,2,(len g))) = (len f) + (len (mid g,2,(len g))) by FINSEQ_1:35;
then A7: ( len f <= (len f) + (len (mid g,2,(len g))) & len f <= len (f ^ (mid g,2,(len g))) ) by NAT_1:11;
A8: len (mid g,2,(len g)) = ((len g) -' 2) + 1 by A3, A5, Th27
.= ((len g) - 2) + 1 by A3, XREAL_1:235
.= (len g) - 1 ;
A9: 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

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 A10: ( 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 ) ; :: thesis: x1 = x2
then A11: ( x1 in Seg (len (f ^ (mid g,2,(len g)))) & x2 in Seg (len (f ^ (mid g,2,(len g)))) ) by FINSEQ_1:def 3;
reconsider n1 = x1, n2 = x2 as Element of NAT by A10;
A12: ( 1 <= n1 & n1 <= len (f ^ (mid g,2,(len g))) & 1 <= n2 & n2 <= len (f ^ (mid g,2,(len g))) ) by A11, FINSEQ_1:3;
then A13: n1 - (len f) <= ((len f) + (len (mid g,2,(len g)))) - (len f) by A6, XREAL_1:11;
A14: n2 - (len f) <= ((len f) + (len (mid g,2,(len g)))) - (len f) by A6, A12, XREAL_1:11;
A15: rng (f ^ (mid g,2,(len g))) c= the carrier of (TOP-REAL 2) by FINSEQ_1:def 4;
(f ^ (mid g,2,(len g))) . x1 in rng (f ^ (mid g,2,(len g))) by A10, FUNCT_1:def 5;
then reconsider q = (f ^ (mid g,2,(len g))) . x1 as Point of (TOP-REAL 2) by A15;
A16: rng f c= L~ f by A2, SPPOL_2:18;
A17: rng (mid g,2,(len g)) c= rng g by Th28;
A18: rng g c= L~ g by A3, SPPOL_2:18;

A19: now

assume A20: ( q in rng f & q in rng (mid g,2,(len g)) ) ; :: thesis: contradiction
then q in rng g by A17;
then A21: q in (L~ f) /\ (L~ g) by A16, A18, A20, XBOOLE_0:def 4;

now

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

end;

hence contradiction by A1, A20, A21, TARSKI:def 1; :: thesis: verum

end;

now

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

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

then A26: n1 in dom f by A12, FINSEQ_3:27;
then A27: (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 A28: n2 in dom f by A12, FINSEQ_3:27;
then (f ^ (mid g,2,(len g))) . x2 = f . n2 by FINSEQ_1:def 7;
hence x1 = x2 by A2, A10, A26, A27, A28, FUNCT_1:def 8; :: thesis: verum

end;

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

then (len f) + 1 <= n2 by NAT_1:13;
then ((len f) + 1) - (len f) <= n2 - (len f) by XREAL_1:11;
then ( 1 <= n2 -' (len f) & n2 -' (len f) <= len (mid g,2,(len g)) ) by A14, NAT_D:39;
then A30: n2 -' (len f) in dom (mid g,2,(len g)) by FINSEQ_3:27;
then A31: (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 A29, XREAL_1:235
.= n2 ;
hence contradiction by A10, A19, A26, A27, A30, A31, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

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

then (len f) + 1 <= n1 by NAT_1:13;
then A33: ((len f) + 1) - (len f) <= n1 - (len f) by XREAL_1:11;
then A34: 1 <= n1 -' (len f) by NAT_D:39;
A35: n1 -' (len f) <= len (mid g,2,(len g)) by A13, A33, NAT_D:39;
then A36: n1 -' (len f) in dom (mid g,2,(len g)) by A34, FINSEQ_3:27;
then A37: (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) <= (n1 -' (len f)) + 2 by NAT_1:11;
then A38: ((n1 -' (len f)) + 2) -' 1 = ((n1 -' (len f)) + 2) - 1 by A34, XREAL_1:235, XXREAL_0:2
.= (n1 -' (len f)) + ((1 + 1) - 1) ;
A39: 1 <= (n1 -' (len f)) + 1 by A34, NAT_D:48;
(n1 -' (len f)) + 1 <= ((len g) - 1) + 1 by A8, A35, XREAL_1:8;
then A40: (n1 -' (len f)) + 1 in dom g by A39, FINSEQ_3:27;
(len f) + (n1 -' (len f)) = (len f) + (n1 - (len f)) by A32, XREAL_1:235
.= n1 ;
then A41: (f ^ (mid g,2,(len g))) . n1 = g . ((n1 -' (len f)) + 1) by A3, A5, A13, A33, A37, A38, Th27;
A42: (len f) + (n1 -' (len f)) = (len f) + (n1 - (len f)) by A32, XREAL_1:235
.= n1 ;

now

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

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

then A43: n2 in dom f by A12, FINSEQ_3:27;
then (f ^ (mid g,2,(len g))) . x2 = f . n2 by FINSEQ_1:def 7;
hence contradiction by A10, A19, A36, A37, A42, A43, FUNCT_1:def 5; :: thesis: verum

end;

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

then (len f) + 1 <= n2 by NAT_1:13;
then A45: ((len f) + 1) - (len f) <= n2 - (len f) by XREAL_1:11;
then A46: 1 <= n2 -' (len f) by NAT_D:39;
A47: ( 1 <= n2 -' (len f) & n2 -' (len f) <= len (mid g,2,(len g)) ) by A14, A45, NAT_D:39;
then n2 -' (len f) in dom (mid g,2,(len g)) by FINSEQ_3:27;
then A48: (f ^ (mid g,2,(len g))) . ((len f) + (n2 -' (len f))) = (mid g,2,(len g)) . (n2 -' (len f)) by FINSEQ_1:def 7;
n2 -' (len f) <= (n2 -' (len f)) + 2 by NAT_1:11;
then A49: ((n2 -' (len f)) + 2) -' 1 = ((n2 -' (len f)) + 2) - 1 by A46, XREAL_1:235, XXREAL_0:2
.= (n2 -' (len f)) + 1 ;
A50: 1 <= (n2 -' (len f)) + 1 by A46, NAT_D:48;
(n2 -' (len f)) + 1 <= ((len g) - 1) + 1 by A8, A47, XREAL_1:8;
then A51: (n2 -' (len f)) + 1 in dom g by A50, FINSEQ_3:27;
(len f) + (n2 -' (len f)) = (len f) + (n2 - (len f)) by A44, XREAL_1:235
.= n2 ;
then (f ^ (mid g,2,(len g))) . n2 = g . ((n2 -' (len f)) + 1) by A3, A5, A14, A45, A48, A49, Th27;
then (n1 -' (len f)) + 1 = (n2 -' (len f)) + 1 by A3, A10, A40, A41, A51, FUNCT_1:def 8;
then n1 - (len f) = n2 -' (len f) by A32, XREAL_1:235;
then n1 - (len f) = n2 - (len f) by A44, 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;

A52: 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 A53: ( 1 <= i & 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))}
then A54: 1 <= i + 1 by NAT_D:48;
A55: 1 <= (i + 1) + 1 by A53, NAT_D:48;
A56: i + 1 <= len (f ^ (mid g,2,(len g))) by A53, NAT_D:47;
A57: i <= len (f ^ (mid g,2,(len g))) by A53, NAT_D:47;
(i + 1) + 1 <= (len f) + (len (mid g,2,(len g))) by A53, FINSEQ_1:35;
then (i + 1) + 1 <= (len f) + (((len g) -' 2) + 1) by A3, A5, Th27;
then (i + 1) + 1 <= (len f) + (((len g) - (1 + 1)) + 1) by A3, XREAL_1:235;
then A58: ((i + 1) + 1) - (len f) <= ((len f) + (((len g) - (1 + 1)) + 1)) - (len f) by XREAL_1:11;
then A59: (((i + 1) - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by XREAL_1:8;
then A60: (((i - (len f)) + 1) + 1) + 1 <= len g ;

now

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

case A61: 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 (i + 1) + 1 <= len f ;
then A62: i + 1 <= len f by NAT_D:46;
then A63: i <= len f by NAT_D:46;
A64: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A53, A57, FINSEQ_4:24;
f /. i = f . i by A53, A63, FINSEQ_4:24;
then A65: (f ^ (mid g,2,(len g))) /. i = f /. i by A53, A63, A64, FINSEQ_1:85;
A66: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A54, A56, FINSEQ_4:24;
f /. (i + 1) = f . (i + 1) by A54, A62, FINSEQ_4:24;
then A67: (f ^ (mid g,2,(len g))) /. (i + 1) = f /. (i + 1) by A54, A62, A66, FINSEQ_1:85;
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 A53, A56, TOPREAL1:def 5;
then A68: LSeg (f ^ (mid g,2,(len g))),i = LSeg f,i by A53, A62, A65, A67, TOPREAL1:def 5;
A69: (f ^ (mid g,2,(len g))) /. ((i + 1) + 1) = (f ^ (mid g,2,(len g))) . ((i + 1) + 1) by A53, A55, FINSEQ_4:24;
f /. ((i + 1) + 1) = f . ((i + 1) + 1) by A55, A61, FINSEQ_4:24;
then A70: 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 A55, A61, A67, A69, FINSEQ_1:85;
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 A53, A54, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),(i + 1) = LSeg f,(i + 1) by A54, A61, A70, 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, A53, A61, A67, A68, 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 A71: i + 2 >= (len f) + 1 by NAT_1:13;

now

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

case A72: 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 A73: (i + 1) + 1 > (len f) + 1 ;
(i + 1) + 1 >= ((len f) + 1) + 1 by A72, NAT_1:13;
then ((i + 1) + 1) - ((len f) + 1) >= (((len f) + 1) + 1) - ((len f) + 1) by XREAL_1:11;
then A74: (i - (len f)) + 1 >= 1 ;
A75: i + 1 >= (len f) + 1 by A73, NAT_1:13;
then A76: i >= len f by XREAL_1:8;
A77: i + 1 >= len f by A75, NAT_D:48;
A78: (((i -' (len f)) + 1) + 1) + 1 <= len g by A60, A76, XREAL_1:235;
then A79: ((i -' (len f)) + 1) + 1 <= len g by NAT_D:46;
then A80: (i -' (len f)) + 1 <= len g by NAT_D:46;
(((i -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by A79, XREAL_1:11;
then (i -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then A81: (i -' (len f)) + 1 <= ((len g) -' 2) + 1 by A3, XREAL_1:235;
then A82: i -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;
A83: (((i + 1) -' (len f)) + 1) + 1 <= len g by A59, A77, XREAL_1:235;
(i - (len f)) + 1 <= ((len g) -' 2) + 1 by A76, A81, XREAL_1:235;
then (i + 1) - (len f) <= ((len g) -' 2) + 1 ;
then A84: (i + 1) -' (len f) <= ((len g) -' 2) + 1 by A77, XREAL_1:235;
A85: (i -' (len f)) + 1 >= 1 by A74, A76, XREAL_1:235;
then A86: ((i -' (len f)) + 1) + 1 >= 1 by NAT_D:48;
then A87: ((i - (len f)) + 1) + 1 >= 1 by A76, XREAL_1:235;
then ((i + 1) - (len f)) + 1 >= 1 ;
then A88: ((i + 1) -' (len f)) + 1 >= 1 by A77, XREAL_1:235;
then A89: (((i + 1) -' (len f)) + 1) + 1 >= 1 by NAT_D:48;
((i + 1) - (len f)) + 1 >= 0 + 1 by A87;
then A90: (i + 1) - (len f) >= 0 by XREAL_1:8;
then A91: (((i + 1) -' (len f)) + 1) + 1 <= len g by A59, XREAL_0:def 2;
A92: ((i + 1) + 1) -' (len f) <= ((len g) - 2) + 1 by A58, A87, XREAL_0:def 2;
((i + 1) - (len f)) + 1 = ((i - (len f)) + 1) + 1 ;
then A93: ((i + 1) - (len f)) + 1 = ((i -' (len f)) + 1) + 1 by A76, XREAL_1:235;
then A94: ((i + 1) -' (len f)) + 1 = ((i -' (len f)) + 1) + 1 by A77, XREAL_1:235;
(((i + 1) + 1) - (len f)) + 1 = (((i + 1) - (len f)) + 1) + 1 ;
then A95: (((i + 1) + 1) - (len f)) + 1 = (((i + 1) -' (len f)) + 1) + 1 by A90, XREAL_0:def 2;
A96: 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 A53, A56, TOPREAL1:def 5;
A97: LSeg g,((i -' (len f)) + 1) = LSeg (g /. ((i -' (len f)) + 1)),(g /. (((i -' (len f)) + 1) + 1)) by A79, A85, TOPREAL1:def 5;
A98: g /. ((i -' (len f)) + 1) = g . ((i -' (len f)) + 1) by A80, A85, FINSEQ_4:24;

A99: now

assume A100: 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 A101: len f < i by NAT_1:13;
then (f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i - (len f)) by A57, Th15;
then (f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i -' (len f)) by A101, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . i = g . (((i -' (len f)) + 2) - 1) by A3, A82, A100, Th31;
hence (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1) ; :: thesis: verum

end;

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;
then A102: i -' (len f) = 0 ;
then i - (len f) = 0 by A76, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1) by A1, A4, A102, FINSEQ_1:85; :: thesis: verum

end;

then A103: (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1) by A53, A57, A98, A99, FINSEQ_4:24;
A104: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A54, A56, FINSEQ_4:24;
A105: g /. (((i -' (len f)) + 1) + 1) = g . (((i -' (len f)) + 1) + 1) by A79, A86, FINSEQ_4:24;

A106: now

assume A107: 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 A108: 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 A56, Th15;
then (f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) -' (len f)) by A108, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . (i + 1) = g . ((((i + 1) -' (len f)) + 2) - 1) by A3, A84, A107, Th31;
hence (f ^ (mid g,2,(len g))) . (i + 1) = g . (((i + 1) -' (len f)) + 1) ; :: thesis: verum

end;

A109: 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 (i + 1) -' (len f) <= 0 by XREAL_1:8;
then A110: (i + 1) -' (len f) = 0 ;
then (i + 1) - (len f) = 0 by A77, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . (i + 1) = g . (((i + 1) -' (len f)) + 1) by A1, A4, A110, FINSEQ_1:85; :: thesis: verum

end;

A111: 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 A53, A54, TOPREAL1:def 5;
A112: LSeg g,(((i + 1) -' (len f)) + 1) = LSeg (g /. (((i + 1) -' (len f)) + 1)),(g /. ((((i + 1) -' (len f)) + 1) + 1)) by A83, A88, TOPREAL1:def 5;
A113: (f ^ (mid g,2,(len g))) /. ((i + 1) + 1) = (f ^ (mid g,2,(len g))) . ((i + 1) + 1) by A53, A55, FINSEQ_4:24;
A114: g /. ((((i + 1) -' (len f)) + 1) + 1) = g . ((((i + 1) -' (len f)) + 1) + 1) by A89, A91, FINSEQ_4:24;

A115: now

assume A116: 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 A117: 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 A53, Th15;
then (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = (mid g,2,(len g)) . (((i + 1) + 1) -' (len f)) by A117, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . (((((i + 1) + 1) -' (len f)) + 2) - 1) by A3, A92, A116, Th31;
hence (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1) ; :: thesis: verum

end;

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 (((i + 1) + 1) -' (len f)) + 1 <= 0 + 1 by NAT_1:13;
then A118: ((i + 1) + 1) -' (len f) <= 0 by XREAL_1:8;
then A119: ((i + 1) + 1) -' (len f) = 0 ;
((i + 1) + 1) - (len f) = 0 by A87, A118, XREAL_0:def 2;
hence (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1) by A1, A4, A119, FINSEQ_1:85; :: thesis: verum

end;

then A120: LSeg (f ^ (mid g,2,(len g))),(i + 1) = LSeg g,(((i + 1) -' (len f)) + 1) by A93, A95, A104, A105, A106, A109, A111, A112, A113, A114, A115, XREAL_0:def 2;
((i -' (len f)) + 1) + (1 + 1) <= len g by A78;
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, A85, A94, A96, A97, A103, A104, A105, A106, A120, TOPREAL1:def 8; :: thesis: verum

end;

case A121: 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 A122: i <= len f by NAT_D:46;
i = (len f) - 1 by A121;
then A123: i = (len f) -' 1 by A2, XREAL_1:235, XXREAL_0:2;
A124: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A53, A57, FINSEQ_4:24;
f /. i = f . i by A53, A122, FINSEQ_4:24;
then A125: (f ^ (mid g,2,(len g))) /. i = f /. i by A53, A122, A124, FINSEQ_1:85;
A126: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A54, A56, FINSEQ_4:24;
A127: f /. (i + 1) = f . (i + 1) by A54, A121, FINSEQ_4:24;
then A128: f /. (i + 1) = g /. 1 by A1, A5, A121, FINSEQ_4:24;
A129: (f ^ (mid g,2,(len g))) /. (i + 1) = f /. (i + 1) by A54, A121, A126, A127, FINSEQ_1:85;
A130: 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 A53, A56, TOPREAL1:def 5;
A131: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A53, A121, TOPREAL1:def 5;
A132: 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 A53, A54, TOPREAL1:def 5;
A133: ((i + 1) -' (len f)) + 1 = 0 + 1 by A121, XREAL_1:234
.= 1 ;
then A134: LSeg g,(((i + 1) -' (len f)) + 1) = LSeg (g /. (((i + 1) -' (len f)) + 1)),(g /. ((((i + 1) -' (len f)) + 1) + 1)) by A3, TOPREAL1:def 5;
A135: (f ^ (mid g,2,(len g))) /. ((i + 1) + 1) = (f ^ (mid g,2,(len g))) . ((i + 1) + 1) by A53, A55, FINSEQ_4:24;
A136: g /. ((((i + 1) -' (len f)) + 1) + 1) = g . ((((i + 1) -' (len f)) + 1) + 1) by A3, A133, FINSEQ_4:24;
(len g) - 2 >= 0 by A3, XREAL_1:50;
then A137: 0 + 1 <= ((len g) - 2) + 1 by XREAL_1:8;
len f < (i + 1) + 1 by A121, NAT_1:13;
then (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = (mid g,2,(len g)) . (((i + 1) + 1) - (len f)) by A53, Th15;
then A138: (f ^ (mid g,2,(len g))) . ((i + 1) + 1) = g . ((2 + 1) -' 1) by A3, A121, A137, Th31
.= g . 2 by NAT_D:34 ;
A139: LSeg g,1 = LSeg (g /. 1),(g /. (1 + 1)) by A3, TOPREAL1:def 5;
A140: g /. 1 = g . 1 by A5, FINSEQ_4:24;
then g /. 1 = f /. (len f) by A1, A4, FINSEQ_4:24;
then A141: g /. 1 in LSeg (f /. ((len f) -' 1)),(f /. (len f)) by RLTOPSP1:69;
g /. 1 in LSeg (g /. 1),(g /. (1 + 1)) by RLTOPSP1:69;
then g /. 1 in (LSeg f,i) /\ (LSeg g,1) by A121, A123, A131, A139, A141, XBOOLE_0:def 4;
then A142: {(g /. 1)} c= (LSeg f,i) /\ (LSeg g,1) by ZFMISC_1:37;
A143: LSeg f,i c= L~ f by TOPREAL3:26;
LSeg g,1 c= L~ g by TOPREAL3:26;
then (LSeg f,i) /\ (LSeg g,1) c= {(g /. 1)} by A1, A140, A143, XBOOLE_1:27;
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 A125, A128, A129, A130, A131, A132, A133, A134, A135, A136, A138, A142, 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;

A144: 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 A145: 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 A146: ( 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 A147: j <= len (f ^ (mid g,2,(len g))) by NAT_D:46;
then A148: i + 1 < len (f ^ (mid g,2,(len g))) by A145, XXREAL_0:2;
then A149: i <= len (f ^ (mid g,2,(len g))) by NAT_D:46;
A150: i + 1 < len f by A145, A146, XXREAL_0:2;
then A151: i < len f by NAT_1:13;

now

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

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

then A153: 1 <= i + 1 by NAT_D:48;
then A154: 1 < j by A145, XXREAL_0:2;
then A155: 1 <= j + 1 by NAT_D:48;
A156: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by A149, A152, FINSEQ_4:24;
f /. i = f . i by A151, A152, FINSEQ_4:24;
then A157: (f ^ (mid g,2,(len g))) /. i = f /. i by A151, A152, A156, FINSEQ_1:85;
A158: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A148, A153, FINSEQ_4:24;
f /. (i + 1) = f . (i + 1) by A150, A153, FINSEQ_4:24;
then A159: LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f /. i),(f /. (i + 1)) by A150, A153, A157, A158, FINSEQ_1:85;
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 A148, A152, TOPREAL1:def 5;
then A160: LSeg (f ^ (mid g,2,(len g))),i = LSeg f,i by A150, A152, A159, TOPREAL1:def 5;
A161: j + 1 <= len f by A146, NAT_1:13;
A162: (f ^ (mid g,2,(len g))) /. j = (f ^ (mid g,2,(len g))) . j by A147, A154, FINSEQ_4:24;
f /. j = f . j by A146, A154, FINSEQ_4:24;
then A163: (f ^ (mid g,2,(len g))) /. j = f /. j by A146, A154, A162, FINSEQ_1:85;
A164: (f ^ (mid g,2,(len g))) /. (j + 1) = (f ^ (mid g,2,(len g))) . (j + 1) by A146, A155, FINSEQ_4:24;
f /. (j + 1) = f . (j + 1) by A155, A161, FINSEQ_4:24;
then A165: LSeg ((f ^ (mid g,2,(len g))) /. j),((f ^ (mid g,2,(len g))) /. (j + 1)) = LSeg (f /. j),(f /. (j + 1)) by A155, A161, A163, A164, FINSEQ_1:85;
A166: 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 A146, A154, TOPREAL1:def 5;
LSeg f,j = LSeg (f /. j),(f /. (j + 1)) by A154, A161, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j by A2, A145, A160, A165, A166, 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 A167: ( 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 A145, A167, XXREAL_0:1;

case A168: ( 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 A169: i + 1 < len (f ^ (mid g,2,(len g))) by A6, A168, XXREAL_0:2;
A170: 1 + 1 <= j by A2, A168, XXREAL_0:2;
then A171: 1 <= j by NAT_D:46;
A172: len f <= j + 1 by A168, NAT_D:48;

now

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

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

then A174: 1 <= i + 1 by NAT_D:48;
A175: (i + 1) + 1 <= len f by A168, NAT_1:13;

A176: now

( 1 <= i & i <= len (f ^ (mid g,2,(len g))) ) by A169, A173, NAT_D:46;
then A177: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by FINSEQ_4:24;
( 1 <= i & i <= len f ) by A167, A173, NAT_D:46;
then A178: f /. i = f . i by FINSEQ_4:24;
( 1 <= i & i <= len f ) by A167, A173, NAT_D:46;
then A179: (f ^ (mid g,2,(len g))) /. i = f /. i by A177, A178, FINSEQ_1:85;
A180: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A169, A174, FINSEQ_4:24;
f /. (i + 1) = f . (i + 1) by A167, A174, FINSEQ_4:24;
then A181: LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f /. i),(f /. (i + 1)) by A167, A174, A179, A180, FINSEQ_1:85;
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 A169, A173, TOPREAL1:def 5;
hence LSeg (f ^ (mid g,2,(len g))),i = LSeg f,i by A167, A173, A181, TOPREAL1:def 5; :: thesis: verum

end;

A182: 1 <= 1 + (j -' (len f)) by NAT_1:11;
(j + 1) + 1 <= ((len f) + ((len g) - 1)) + 1 by A6, A8, A167, 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 A183: ((j -' (len f)) + 1) + 1 <= len g by A168, XREAL_1:235;
then (((j -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by XREAL_1:11;
then A184: (j -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then (j -' (len f)) + 1 <= ((len g) -' 2) + 1 by A3, XREAL_1:235;
then A185: j -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;
A186: (j -' (len f)) + 1 = (j - (len f)) + 1 by A167, XREAL_1:235
.= (j + 1) - (len f)
.= (j + 1) -' (len f) by A172, XREAL_1:235 ;
A187: LSeg g,((j -' (len f)) + 1) = LSeg (g /. ((j -' (len f)) + 1)),(g /. (((j -' (len f)) + 1) + 1)) by A182, A183, TOPREAL1:def 5;
A188: ( 1 <= j & j <= len (f ^ (mid g,2,(len g))) ) by A167, A170, NAT_D:46;
( 1 <= (j -' (len f)) + 1 & (j -' (len f)) + 1 <= len g ) by A183, NAT_1:11, NAT_D:46;
then A189: g /. ((j -' (len f)) + 1) = g . ((j -' (len f)) + 1) by FINSEQ_4:24;

A190: now

assume A191: 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 A192: len f < j by NAT_1:13;
then (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j - (len f)) by A188, Th15;
then (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j -' (len f)) by A192, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . j = g . (((j -' (len f)) + 2) - 1) by A3, A185, A191, Th31;
hence (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1) ; :: thesis: verum

end;

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 j -' (len f) <= 0 by XREAL_1:8;
then A193: j -' (len f) = 0 ;
then j - (len f) = 0 by A167, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1) by A1, A4, A193, FINSEQ_1:85; :: thesis: verum

end;

then A194: (f ^ (mid g,2,(len g))) /. j = g /. ((j -' (len f)) + 1) by A188, A189, A190, FINSEQ_4:24;
( 1 <= j + 1 & j + 1 <= len (f ^ (mid g,2,(len g))) ) by A167, A171, NAT_D:48;
then A195: (f ^ (mid g,2,(len g))) /. (j + 1) = (f ^ (mid g,2,(len g))) . (j + 1) by FINSEQ_4:24;
A196: g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by A183, FINSEQ_4:24, NAT_1:11;

A197: now

assume A198: 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 A199: 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 A167, Th15;
then (f ^ (mid g,2,(len g))) . (j + 1) = (mid g,2,(len g)) . ((j + 1) -' (len f)) by A199, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . (j + 1) = g . ((((j + 1) -' (len f)) + 2) - 1) by A3, A184, A186, A198, Th31;
hence (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) ; :: thesis: verum

end;

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 (j + 1) -' (len f) <= 0 by XREAL_1:8;
then A200: (j + 1) -' (len f) = 0 ;
then (j + 1) - (len f) = 0 by A172, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) by A1, A4, A200, FINSEQ_1:85; :: thesis: verum

end;

then A201: LSeg (f ^ (mid g,2,(len g))),j = LSeg g,((j -' (len f)) + 1) by A167, A171, A186, A187, A194, A195, A196, A197, TOPREAL1:def 5;
A202: LSeg (f ^ (mid g,2,(len g))),i c= L~ f by A176, TOPREAL3:26;
LSeg (f ^ (mid g,2,(len g))),j c= L~ g by A201, TOPREAL3:26;
then A203: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) c= {(g . 1)} by A1, A202, XBOOLE_1:27;

now

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

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

A205: (1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
A206: 1 <= len f by A2, XXREAL_0:2;
A207: ((len f) -' 1) + 1 = ((len f) - 1) + 1 by A2, XREAL_1:235, XXREAL_0:2
.= len f ;

now

given x being set such that A208: x in (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) ; :: thesis: contradiction
A209: x = g . 1 by A203, A208, TARSKI:def 1;
A210: x in LSeg f,i by A176, A208, XBOOLE_0:def 4;
f /. (len f) in LSeg f,((len f) -' 1) by A205, A207, TOPREAL1:27;
then g . 1 in LSeg f,((len f) -' 1) by A1, A206, FINSEQ_4:24;
then x in (LSeg f,i) /\ (LSeg f,((len f) -' 1)) by A209, A210, XBOOLE_0:def 4;
then LSeg f,i meets LSeg f,((len f) -' 1) by XBOOLE_0:4;
hence contradiction by A2, A204, 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 A2, XREAL_1:235, XXREAL_0:2;
then A211: (i + 1) + 1 >= ((len f) - 1) + 1 by XREAL_1:8;
then A212: (i + 1) + 1 = len f by A175, XXREAL_0:1;
then i + 1 = (len f) - 1 ;
then A213: ( i + 1 = (len f) - 1 & i + 1 = (len f) -' 1 ) by A2, XREAL_1:235, XXREAL_0:2;
A214: ( (i + 1) + 1 = len f & i + (1 + 1) = len f ) by A175, A211, XXREAL_0:1;
A215: ( (i + 1) + 1 = len f & i + (1 + 1) = len f & 1 <= i + 1 & i + 1 <= len f ) by A212, NAT_1:11;
A216: ((len f) -' 1) + 1 = ((len f) - 1) + 1 by A2, XREAL_1:235, XXREAL_0:2
.= len f ;
then 1 + 1 <= ((len f) -' 1) + 1 by A1, TOPREAL1:def 10;
then A217: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 <= len f ) by A216, XREAL_1:8;

now

given x being set such that A218: x in (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) ; :: thesis: contradiction
A219: x = g . 1 by A203, A218, TARSKI:def 1;
A220: x in LSeg f,i by A176, A218, XBOOLE_0:def 4;
f /. (len f) in LSeg f,((len f) -' 1) by A216, A217, TOPREAL1:27;
then g . 1 in LSeg f,((len f) -' 1) by A1, A4, FINSEQ_4:24;
then A221: x in (LSeg f,i) /\ (LSeg f,((len f) -' 1)) by A219, A220, XBOOLE_0:def 4;
(LSeg f,i) /\ (LSeg f,((len f) -' 1)) = {(f /. (i + 1))} by A2, A173, A213, A214, TOPREAL1:def 8;
then f . (len f) = f /. (i + 1) by A1, A219, A221, TARSKI:def 1;
then A222: f . (len f) = f . ((len f) -' 1) by A213, A215, FINSEQ_4:24;
A223: len f in dom f by A4, FINSEQ_3:27;
A224: (len f) -' 1 <= len f by NAT_D:35;
(1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then 1 <= (len f) -' 1 by NAT_D:39;
then (len f) -' 1 in dom f by A224, FINSEQ_3:27;
then len f = (len f) -' 1 by A2, A222, A223, FUNCT_1:def 8;
then len f = (len f) - 1 by A2, 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 A225: ( 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)))

proof

(1 + 1) - 1 <= (len g) - 1 by A3, XREAL_1:11;
then (len f) + 1 <= (len f) + (len (mid g,2,(len g))) by A8, XREAL_1:9;
hence len f < (len f) + (len (mid g,2,(len g))) by NAT_1:13; :: thesis: verum

end;

then A226: i + 1 < len (f ^ (mid g,2,(len g))) by A6, A225, XXREAL_0:2;
A227: 1 + 1 <= j by A2, A225, XXREAL_0:2;
then A228: 1 <= j by NAT_D:46;
A229: len f <= j + 1 by A225, NAT_D:48;

now

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

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

then A231: 1 <= i + 1 by NAT_D:48;

A232: now

( 1 <= i & i <= len (f ^ (mid g,2,(len g))) ) by A226, A230, NAT_D:46;
then A233: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by FINSEQ_4:24;
( 1 <= i & i <= len f ) by A167, A230, NAT_D:46;
then A234: f /. i = f . i by FINSEQ_4:24;
( 1 <= i & i <= len f ) by A167, A230, NAT_D:46;
then A235: (f ^ (mid g,2,(len g))) /. i = f /. i by A233, A234, FINSEQ_1:85;
A236: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A226, A231, FINSEQ_4:24;
f /. (i + 1) = f . (i + 1) by A167, A231, FINSEQ_4:24;
then A237: LSeg ((f ^ (mid g,2,(len g))) /. i),((f ^ (mid g,2,(len g))) /. (i + 1)) = LSeg (f /. i),(f /. (i + 1)) by A167, A231, A235, A236, FINSEQ_1:85;
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 A226, A230, TOPREAL1:def 5;
hence LSeg (f ^ (mid g,2,(len g))),i = LSeg f,i by A167, A230, A237, TOPREAL1:def 5; :: thesis: verum

end;

A238: 1 <= 1 + (j -' (len f)) by NAT_1:11;
(j + 1) + 1 <= ((len f) + ((len g) - 1)) + 1 by A6, A8, A167, 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 A239: ((j -' (len f)) + 1) + 1 <= len g by A225, XREAL_1:235;
then (((j -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by XREAL_1:11;
then A240: (j -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then (j -' (len f)) + 1 <= ((len g) -' 2) + 1 by A3, XREAL_1:235;
then A241: j -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;
A242: (j -' (len f)) + 1 = (j - (len f)) + 1 by A167, XREAL_1:235
.= (j + 1) - (len f)
.= (j + 1) -' (len f) by A229, XREAL_1:235 ;
A243: LSeg g,((j -' (len f)) + 1) = LSeg (g /. ((j -' (len f)) + 1)),(g /. (((j -' (len f)) + 1) + 1)) by A238, A239, TOPREAL1:def 5;
A244: ( 1 <= j & j <= len (f ^ (mid g,2,(len g))) ) by A167, A227, NAT_D:46;
( 1 <= (j -' (len f)) + 1 & (j -' (len f)) + 1 <= len g ) by A239, NAT_1:11, NAT_D:46;
then A245: g /. ((j -' (len f)) + 1) = g . ((j -' (len f)) + 1) by FINSEQ_4:24;

A246: now

assume A247: 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 A248: len f < j by NAT_1:13;
then (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j - (len f)) by A244, Th15;
then (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j -' (len f)) by A248, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . j = g . (((j -' (len f)) + 2) - 1) by A3, A241, A247, Th31;
hence (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1) ; :: thesis: verum

end;

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 j -' (len f) <= 0 by XREAL_1:8;
then A249: j -' (len f) = 0 ;
then j - (len f) = 0 by A167, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . j = g . ((j -' (len f)) + 1) by A1, A4, A249, FINSEQ_1:85; :: thesis: verum

end;

then A250: (f ^ (mid g,2,(len g))) /. j = g /. ((j -' (len f)) + 1) by A244, A245, A246, FINSEQ_4:24;
( 1 <= j + 1 & j + 1 <= len (f ^ (mid g,2,(len g))) ) by A167, A228, NAT_D:48;
then A251: (f ^ (mid g,2,(len g))) /. (j + 1) = (f ^ (mid g,2,(len g))) . (j + 1) by FINSEQ_4:24;
A252: g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by A239, FINSEQ_4:24, NAT_1:11;

A253: now

assume A254: 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 A255: 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 A167, Th15;
then (f ^ (mid g,2,(len g))) . (j + 1) = (mid g,2,(len g)) . ((j + 1) -' (len f)) by A255, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . (j + 1) = g . ((((j + 1) -' (len f)) + 2) - 1) by A3, A240, A242, A254, Th31;
hence (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) ; :: thesis: verum

end;

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 (j + 1) -' (len f) <= 0 by XREAL_1:8;
then A256: (j + 1) -' (len f) = 0 ;
then (j + 1) - (len f) = 0 by A229, XREAL_1:235;
hence (f ^ (mid g,2,(len g))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) by A1, A4, A256, FINSEQ_1:85; :: thesis: verum

end;

then A257: LSeg (f ^ (mid g,2,(len g))),j = LSeg g,((j -' (len f)) + 1) by A167, A228, A242, A243, A250, A251, A252, A253, TOPREAL1:def 5;
A258: LSeg (f ^ (mid g,2,(len g))),i c= L~ f by A232, TOPREAL3:26;
LSeg (f ^ (mid g,2,(len g))),j c= L~ g by A257, TOPREAL3:26;
then A259: (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) c= {(g . 1)} by A1, A258, XBOOLE_1:27;

now

given x being set such that A260: x in (LSeg (f ^ (mid g,2,(len g))),i) /\ (LSeg (f ^ (mid g,2,(len g))),j) ; :: thesis: contradiction
A261: x = g . 1 by A259, A260, TARSKI:def 1;
then A262: g /. 1 = x by A5, FINSEQ_4:24;
A263: ( LSeg g,((j -' (len f)) + 1) <> {} & x in LSeg g,((j -' (len f)) + 1) & 1 + 1 <= len g ) by A1, A257, A260, TOPREAL1:def 10, XBOOLE_0:def 4;
then ( x in LSeg g,1 & x in LSeg g,((j -' (len f)) + 1) ) by A262, TOPREAL1:27;
then A264: x in (LSeg g,1) /\ (LSeg g,((j -' (len f)) + 1)) by 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 1 + (len f) >= (j - (len f)) + (len f) by XREAL_1:8;
then ( (len f) + 1 >= j & j >= (len f) + 1 ) by A225, NAT_1:13;
then A265: ( j = (len f) + 1 & (j -' (len f)) + 1 = (j - (len f)) + 1 ) by A225, XREAL_1:235, XXREAL_0:1;
then 1 + 2 <= len g by A263, TOPREAL1:def 5;
then (LSeg g,1) /\ (LSeg g,((j -' (len f)) + 1)) = {(g /. (1 + 1))} by A3, A265, TOPREAL1:def 8;
then A266: x = g /. (1 + 1) by A264, TARSKI:def 1
.= g . (1 + 1) by A3, FINSEQ_4:24 ;
A267: 1 in dom g by A5, FINSEQ_3:27;
1 + 1 in dom g by A3, FINSEQ_3:27;
hence contradiction by A3, A261, A266, A267, 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 A268: ( 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 A269: len f <= i by NAT_1:13;
then A270: 1 + 1 <= i by A2, XXREAL_0:2;
then A271: 1 <= i by NAT_D:46;
then A272: 1 <= i + 1 by NAT_D:48;
then A273: 1 <= j by A145, XXREAL_0:2;
A274: len f < j by A145, A268, XXREAL_0:2;
j <= j + 1 by NAT_1:11;
then A275: len f < j + 1 by A274, XXREAL_0:2;
A276: i -' (len f) = i - (len f) by A269, XREAL_1:235;
A277: j -' (len f) = j - (len f) by A145, A268, XREAL_1:235, XXREAL_0:2;
(i + 1) - (len f) < j - (len f) by A145, XREAL_1:11;
then A278: ((i -' (len f)) + 1) + 1 < (j -' (len f)) + 1 by A276, A277, XREAL_1:8;
A279: 1 <= (i -' (len f)) + 1 by NAT_1:11;
A280: 1 <= (j -' (len f)) + 1 by NAT_1:11;

now

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

case A281: 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 A282: j <= len (f ^ (mid g,2,(len g))) by NAT_D:46;

A283: now

A284: i + 1 < len (f ^ (mid g,2,(len g))) by A145, A282, XXREAL_0:2;
then i + 1 < (len f) + ((len g) - 1) by A8, FINSEQ_1:35;
then A285: (i + 1) - (len f) < ((len f) + ((len g) - 1)) - (len f) by XREAL_1:11;
then A286: ((i - (len f)) + 1) + 1 < ((len g) - 1) + 1 by XREAL_1:8;
then A287: (i -' (len f)) + 1 <= len g by A276, NAT_D:46;
A288: (i -' (len f)) + 1 <= ((len g) - 2) + 1 by A276, A285;
A289: ( 1 <= i & i <= len (f ^ (mid g,2,(len g))) ) by A270, A284, NAT_D:46;
A290: g /. ((i -' (len f)) + 1) = g . ((i -' (len f)) + 1) by A287, FINSEQ_4:24, NAT_1:11;

A291: 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 A292: i = len f by A269, XXREAL_0:1;
then (f ^ (mid g,2,(len g))) . i = g . (0 + 1) by A1, A271, FINSEQ_1:85
.= g . ((i -' (len f)) + 1) by A292, XREAL_1:234 ;
hence (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1) by A289, A290, FINSEQ_4:24; :: thesis: verum

end;

case A293: 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 A294: ((len f) + 1) - (len f) <= i - (len f) by XREAL_1:11;
((i -' (len f)) + 1) - 1 <= (len g) - 1 by A287, XREAL_1:11;
then A295: i -' (len f) <= ((len g) - 2) + 1 ;
(f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i -' (len f)) by A276, A289, A293, Th15
.= g . (((i -' (len f)) + 2) - 1) by A3, A276, A294, A295, Th31
.= g . ((i -' (len f)) + 1) ;
hence (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1) by A289, A290, FINSEQ_4:24; :: thesis: verum

end;

end;

end;

( 1 <= i + 1 & i + 1 <= len (f ^ (mid g,2,(len g))) ) by A145, A282, A289, NAT_D:48, XXREAL_0:2;
then A296: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by FINSEQ_4:24;
( 1 <= ((i -' (len f)) + 1) + 1 & ((i -' (len f)) + 1) + 1 <= len g ) by A269, A286, NAT_1:11, XREAL_1:235;
then A297: g /. (((i -' (len f)) + 1) + 1) = g . (((i -' (len f)) + 1) + 1) by FINSEQ_4:24;
A298: (((i -' (len f)) + 1) + 2) - 1 = ((i -' (len f)) + 1) + 1 ;
A299: (f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) - (len f)) by A268, A284, Th15
.= g . (((i -' (len f)) + 1) + 1) by A3, A276, A279, A288, A298, Th31 ;
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 A271, A284, TOPREAL1:def 5;
hence LSeg (f ^ (mid g,2,(len g))),i = LSeg g,((i -' (len f)) + 1) by A276, A279, A286, A291, A296, A297, A299, TOPREAL1:def 5; :: thesis: verum

end;

j + 1 <= (len f) + ((len g) - 1) by A8, A281, FINSEQ_1:35;
then A300: (j + 1) - (len f) <= ((len f) + ((len g) - 1)) - (len f) by XREAL_1:11;
then A301: ((j - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by XREAL_1:8;
then A302: (j -' (len f)) + 1 <= len g by A277, NAT_D:46;
A303: (j -' (len f)) + 1 <= ((len g) - 2) + 1 by A277, A300;
A304: ( 1 <= j & j <= len (f ^ (mid g,2,(len g))) ) by A145, A272, A281, NAT_D:46, XXREAL_0:2;
then A305: (f ^ (mid g,2,(len g))) /. j = (f ^ (mid g,2,(len g))) . j by FINSEQ_4:24;
A306: g /. ((j -' (len f)) + 1) = g . ((j -' (len f)) + 1) by A302, FINSEQ_4:24, NAT_1:11;
(len f) + 1 <= j by A274, NAT_1:13;
then A307: ((len f) + 1) - (len f) <= j - (len f) by XREAL_1:11;
((j -' (len f)) + 1) - 1 <= (len g) - 1 by A302, XREAL_1:11;
then A308: j -' (len f) <= ((len g) - 2) + 1 ;
A309: (f ^ (mid g,2,(len g))) . j = (mid g,2,(len g)) . (j - (len f)) by A274, A304, Th15
.= g . (((j -' (len f)) + 2) - 1) by A3, A277, A307, A308, Th31
.= g . ((j -' (len f)) + 1) ;
( 1 <= j + 1 & j + 1 <= len (f ^ (mid g,2,(len g))) ) by A281, A304, NAT_D:48;
then A310: (f ^ (mid g,2,(len g))) /. (j + 1) = (f ^ (mid g,2,(len g))) . (j + 1) by FINSEQ_4:24;
( 1 <= ((j -' (len f)) + 1) + 1 & ((j -' (len f)) + 1) + 1 <= len g ) by A274, A301, NAT_1:11, XREAL_1:235;
then A311: g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by FINSEQ_4:24;
A312: (((j -' (len f)) + 1) + 2) - 1 = ((j -' (len f)) + 1) + 1 ;
A313: (f ^ (mid g,2,(len g))) . (j + 1) = (mid g,2,(len g)) . ((j + 1) - (len f)) by A275, A281, Th15
.= g . (((j -' (len f)) + 1) + 1) by A3, A277, A280, A303, A312, Th31 ;
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 A273, A281, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),j = LSeg g,((j -' (len f)) + 1) by A277, A280, A301, A305, A306, A309, A310, A311, A313, TOPREAL1:def 5;
then LSeg (f ^ (mid g,2,(len g))),i misses LSeg (f ^ (mid g,2,(len g))),j by A3, A278, A283, 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;

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 A314: ( 1 <= i & 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 A315: 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 )

A316: 1 <= i + 1 by A314, NAT_D:48;
A317: i + 1 <= len f by A315, NAT_1:13;
( 1 <= i & i <= len (f ^ (mid g,2,(len g))) ) by A314, NAT_D:46;
then A318: (f ^ (mid g,2,(len g))) /. i = (f ^ (mid g,2,(len g))) . i by FINSEQ_4:24;
f /. i = f . i by A314, A315, FINSEQ_4:24;
then A319: (f ^ (mid g,2,(len g))) /. i = f /. i by A314, A315, A318, FINSEQ_1:85;
A320: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by A314, A316, FINSEQ_4:24;
A321: f /. (i + 1) = f . (i + 1) by A316, A317, FINSEQ_4:24;
(f ^ (mid g,2,(len g))) . (i + 1) = f . (i + 1) by A316, A317, FINSEQ_1:85;
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, A314, A317, A319, A320, A321, TOPREAL1:def 7; :: thesis: verum

end;

case A322: 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 )

then A323: i - (len f) >= 0 by XREAL_1:50;
then A324: i -' (len f) = i - (len f) by XREAL_0:def 2;
A325: i + 1 >= len f by A322, NAT_D:48;
A326: (i + 1) - (len f) <= ((len f) + ((len g) - 1)) - (len f) by A6, A8, A314, XREAL_1:11;
then A327: ((i - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by XREAL_1:8;
then A328: ( 1 <= (i -' (len f)) + 1 & ((i -' (len f)) + 1) + 1 <= len g ) by A323, NAT_1:11, XREAL_0:def 2;
i -' (len f) <= (i -' (len f)) + 1 by NAT_1:11;
then A329: i -' (len f) <= ((len g) - 2) + 1 by A324, A326, XXREAL_0:2;
A330: ( 1 <= i & i <= len (f ^ (mid g,2,(len g))) ) by A314, NAT_D:46;
( 1 <= (i -' (len f)) + 1 & (i -' (len f)) + 1 <= len g ) by A324, A327, NAT_1:11, NAT_D:46;
then A331: g /. ((i -' (len f)) + 1) = g . ((i -' (len f)) + 1) by FINSEQ_4:24;
(i + 1) - (len f) <= ((len g) - 2) + 1 by A326;
then (i + 1) - (len f) <= ((len g) -' 2) + 1 by A3, XREAL_1:235;
then A332: (i + 1) -' (len f) <= ((len g) -' 2) + 1 by A325, XREAL_1:235;
A333: ((i + 1) -' (len f)) + 1 = ((i + 1) - (len f)) + 1 by A325, XREAL_1:235
.= ((i - (len f)) + 1) + 1
.= ((i -' (len f)) + 1) + 1 by A322, XREAL_1:235 ;
1 <= 1 + (i -' (len f)) by NAT_1:11;
then 1 <= 1 + (i - (len f)) by A322, XREAL_1:235;
then 1 <= (1 + i) - (len f) ;
then A334: 1 <= (i + 1) -' (len f) by NAT_D:39;

A335: now

assume A336: 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 A337: len f < i by NAT_1:13;
then (f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i - (len f)) by A330, Th15;
then (f ^ (mid g,2,(len g))) . i = (mid g,2,(len g)) . (i -' (len f)) by A337, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . i = g . (((i -' (len f)) + 2) - 1) by A3, A329, A336, Th31;
hence (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1) ; :: thesis: verum

end;

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;
then i -' (len f) = 0 ;
hence (f ^ (mid g,2,(len g))) . i = g . ((i -' (len f)) + 1) by A1, A4, A324, FINSEQ_1:85; :: thesis: verum

end;

then A338: (f ^ (mid g,2,(len g))) /. i = g /. ((i -' (len f)) + 1) by A330, A331, A335, FINSEQ_4:24;
( 1 <= i + 1 & i + 1 <= len (f ^ (mid g,2,(len g))) ) by A314, NAT_D:48;
then A339: (f ^ (mid g,2,(len g))) /. (i + 1) = (f ^ (mid g,2,(len g))) . (i + 1) by FINSEQ_4:24;
( 1 <= ((i -' (len f)) + 1) + 1 & ((i -' (len f)) + 1) + 1 <= len g ) by A323, A327, NAT_1:11, XREAL_0:def 2;
then A340: g /. (((i -' (len f)) + 1) + 1) = g . (((i -' (len f)) + 1) + 1) by FINSEQ_4:24;
len f < i + 1 by A322, NAT_1:13;
then (f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) - (len f)) by A314, Th15;
then (f ^ (mid g,2,(len g))) . (i + 1) = (mid g,2,(len g)) . ((i + 1) -' (len f)) by A325, XREAL_1:235;
then (f ^ (mid g,2,(len g))) . (i + 1) = g . ((((i + 1) -' (len f)) + 2) - 1) by A3, A332, A334, Th31;
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, A328, A333, A338, A339, A340, 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 one-to-one & len (f ^ (mid g,2,(len g))) >= 2 & 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 A2, A7, A9, A52, A144, FUNCT_1:def 8, TOPREAL1:def 7, TOPREAL1:def 8, TOPREAL1:def 9, XXREAL_0:2;
hence f ^ (mid g,2,(len g)) is being_S-Seq by TOPREAL1:def 10; :: thesis: verum