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 8;
A6: len (f ^ (mid (g,2,(len g)))) = (len f) + (len (mid (g,2,(len g)))) by FINSEQ_1:22;
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 8;
then A9: 1 <= len g by XXREAL_0:2;
then A10: len (mid (g,2,(len g))) = ((len g) -' 2) + 1 by A8, FINSEQ_6:118
.= ((len g) - 2) + 1 by A8, XREAL_1:233
.= (len g) - 1 ;
for x1, x2 being object 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 object ; :: 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:1;
(f ^ (mid (g,2,(len g)))) . x1 in rng (f ^ (mid (g,2,(len g)))) by A13, FUNCT_1:def 3;
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 FINSEQ_6:119;
A19: rng f c= L~ f by A5, SPPOL_2:18;
A20: now :: thesis: ( q in rng f implies not q in rng (mid (g,2,(len g))) )
A21: now :: thesis: not g . 1 in rng (mid (g,2,(len g)))
g | 1 = g | (Seg 1) by FINSEQ_1:def 16;
then A22: (g | 1) . 1 = g . 1 by FINSEQ_1:3, FUNCT_1:49;
len (g | 1) = 1 by A8, FINSEQ_1:59, XXREAL_0:2;
then 1 in dom (g | 1) by FINSEQ_3:25;
then A23: g . 1 in rng (g | 1) by A22, FUNCT_1:def 3;
A24: 2 -' 1 = 2 - 1 by XREAL_1:233;
assume g . 1 in rng (mid (g,2,(len g))) ; :: thesis: contradiction
then A25: g . 1 in rng (g /^ 1) by A8, A24, FINSEQ_6:117;
rng (g | 1) misses rng (g /^ 1) by A3, FINSEQ_5:34;
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:1;
then A28: n2 - (len f) <= ((len f) + (len (mid (g,2,(len g))))) - (len f) by A6, XREAL_1:9;
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:1;
then A30: n1 - (len f) <= ((len f) + (len (mid (g,2,(len g))))) - (len f) by A6, XREAL_1:9;
A31: 1 <= n1 by A29, FINSEQ_1:1;
now :: thesis: ( ( n1 <= len f & x1 = x2 ) or ( n1 > len f & x1 = x2 ) )
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:25;
then A33: (f ^ (mid (g,2,(len g)))) . x1 = f . n1 by FINSEQ_1:def 7;
now :: thesis: ( ( n2 <= len f & x1 = x2 ) or ( n2 > len f & contradiction ) )
per cases ( n2 <= len f or n2 > len f ) ;
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:9;
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:233
.= 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:25;
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 3; :: 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:9;
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:233, XXREAL_0:2
.= (n1 -' (len f)) + ((1 + 1) - 1) ;
A45: (len f) + (n1 -' (len f)) = (len f) + (n1 - (len f)) by A40, XREAL_1:233
.= 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:25;
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:6;
then A49: (n1 -' (len f)) + 1 in dom g by A43, FINSEQ_3:25;
(len f) + (n1 -' (len f)) = (len f) + (n1 - (len f)) by A40, XREAL_1:233
.= n1 ;
then A50: (f ^ (mid (g,2,(len g)))) . n1 = g . ((n1 -' (len f)) + 1) by A8, A9, A30, A41, A48, A44, FINSEQ_6:118;
now :: thesis: ( ( n2 <= len f & contradiction ) or ( n2 > len f & x1 = x2 ) )
per cases ( n2 <= len f or n2 > len f ) ;
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:9;
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:6;
then A57: (n2 -' (len f)) + 1 in dom g by A55, FINSEQ_3:25;
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:233, 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:25;
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:233
.= n2 ;
then (f ^ (mid (g,2,(len g)))) . n2 = g . ((n2 -' (len f)) + 1) by A8, A9, A28, A53, A59, A58, FINSEQ_6:118;
then (n1 -' (len f)) + 1 = (n2 -' (len f)) + 1 by A3, A15, A49, A50, A57, FUNCT_1:def 4;
then n1 - (len f) = n2 -' (len f) by A40, XREAL_1:233;
then n1 - (len f) = n2 - (len f) by A52, XREAL_1:233;
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 4;
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 :: thesis: ( ( j < len f & j + 1 <= len (f ^ (mid (g,2,(len g)))) & LSeg ((f ^ (mid (g,2,(len g)))),i) misses LSeg ((f ^ (mid (g,2,(len g)))),j) ) or ( i + 1 <= len f & len f <= j & j + 1 <= len (f ^ (mid (g,2,(len g)))) & LSeg ((f ^ (mid (g,2,(len g)))),i) misses LSeg ((f ^ (mid (g,2,(len g)))),j) ) or ( len f < i + 1 & j + 1 <= len (f ^ (mid (g,2,(len g)))) & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) or ( j + 1 > len (f ^ (mid (g,2,(len g)))) & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) )
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 :: thesis: ( ( 1 <= i & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) or ( i < 1 & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) )
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:15;
(f ^ (mid (g,2,(len g)))) /. i = (f ^ (mid (g,2,(len g)))) . i by A69, A70, FINSEQ_4:15;
then A72: (f ^ (mid (g,2,(len g)))) /. i = f /. i by A66, A70, A71, FINSEQ_1:64;
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 3;
A74: 1 <= i + 1 by A70, NAT_D:48;
then A75: f /. (i + 1) = f . (i + 1) by A65, FINSEQ_4:15;
(f ^ (mid (g,2,(len g)))) /. (i + 1) = (f ^ (mid (g,2,(len g)))) . (i + 1) by A68, A74, FINSEQ_4:15;
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:64;
then A76: LSeg ((f ^ (mid (g,2,(len g)))),i) = LSeg (f,i) by A65, A70, A73, TOPREAL1:def 3;
A77: 1 < j by A63, A74, XXREAL_0:2;
then A78: f /. j = f . j by A64, FINSEQ_4:15;
(f ^ (mid (g,2,(len g)))) /. j = (f ^ (mid (g,2,(len g)))) . j by A67, A77, FINSEQ_4:15;
then A79: (f ^ (mid (g,2,(len g)))) /. j = f /. j by A64, A77, A78, FINSEQ_1:64;
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:15;
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 3;
f /. (j + 1) = f . (j + 1) by A80, A82, FINSEQ_4:15;
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:64;
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 3;
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 7;
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 3;
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 :: thesis: ( ( i + 1 < len f & len f <= j & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) or ( i + 1 <= len f & len f < j & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) )
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 :: thesis: ( ( 1 <= i & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) or ( i < 1 & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) )
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:15;
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:15;
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:64;
A95: j <= len (f ^ (mid (g,2,(len g)))) by A85, NAT_D:46;
A96: now :: thesis: ( 1 > j -' (len f) implies (f ^ (mid (g,2,(len g)))) . j = g . ((j -' (len f)) + 1) )
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:6;
then j - (len f) = 0 by A85, XREAL_1:233;
hence (f ^ (mid (g,2,(len g)))) . j = g . ((j -' (len f)) + 1) by A1, A61, A97, FINSEQ_1:64; :: 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:15;
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 3;
A100: 1 <= i + 1 by A91, NAT_D:48;
then A101: f /. (i + 1) = f . (i + 1) by A85, FINSEQ_4:15;
A102: now :: thesis: ( 1 > (j + 1) -' (len f) implies (f ^ (mid (g,2,(len g)))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) )
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:6;
then (j + 1) - (len f) = 0 by A88, XREAL_1:233;
hence (f ^ (mid (g,2,(len g)))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) by A1, A61, A103, FINSEQ_1:64; :: thesis: verum
end;
(j + 1) + 1 <= ((len f) + ((len g) - 1)) + 1 by A6, A10, A85, XREAL_1:6;
then ((j + 1) + 1) - (len f) <= ((len f) + (len g)) - (len f) by XREAL_1:9;
then ((j - (len f)) + 1) + 1 <= len g ;
then A104: ((j -' (len f)) + 1) + 1 <= len g by A86, XREAL_1:233;
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:15, NAT_1:11;
(((j -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by A104, XREAL_1:9;
then A106: (j -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then (j -' (len f)) + 1 <= ((len g) -' 2) + 1 by A8, XREAL_1:233;
then A107: j -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;
A108: now :: thesis: ( 1 <= j -' (len f) implies (f ^ (mid (g,2,(len g)))) . j = g . ((j -' (len f)) + 1) )
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:6;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . j = (mid (g,2,(len g))) . (j -' (len f)) by A110, XREAL_1:233;
then (f ^ (mid (g,2,(len g)))) . j = g . (((j -' (len f)) + 2) - 1) by A8, A107, A109, FINSEQ_6:122;
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:233
.= (j + 1) - (len f)
.= (j + 1) -' (len f) by A88, XREAL_1:233 ;
A112: now :: thesis: ( 1 <= (j + 1) -' (len f) implies (f ^ (mid (g,2,(len g)))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) )
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:6;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . (j + 1) = (mid (g,2,(len g))) . ((j + 1) -' (len f)) by A114, XREAL_1:233;
then (f ^ (mid (g,2,(len g)))) . (j + 1) = g . ((((j + 1) -' (len f)) + 2) - 1) by A8, A106, A111, A113, FINSEQ_6:122;
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 3;
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:15;
g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by A104, FINSEQ_4:15, 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 3;
then A117: LSeg ((f ^ (mid (g,2,(len g)))),j) c= L~ g by TOPREAL3:19;
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:15;
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:64;
then A119: LSeg ((f ^ (mid (g,2,(len g)))),i) = LSeg (f,i) by A85, A91, A99, TOPREAL1:def 3;
then LSeg ((f ^ (mid (g,2,(len g)))),i) c= L~ f by TOPREAL3:19;
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 :: thesis: ( ( i + 1 < (len f) -' 1 & LSeg ((f ^ (mid (g,2,(len g)))),i) misses LSeg ((f ^ (mid (g,2,(len g)))),j) ) or ( i + 1 >= (len f) -' 1 & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) )
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:233, XXREAL_0:2
.= len f ;
A124: (1 + 1) - 1 <= (len f) - 1 by A5, XREAL_1:9;
now :: thesis: for x being object holds not x in (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j))
f /. (len f) in LSeg (f,((len f) -' 1)) by A124, A123, TOPREAL1:21;
then A125: g . 1 in LSeg (f,((len f) -' 1)) by A1, A122, FINSEQ_4:15;
given x being object 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 7; :: 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:233, XXREAL_0:2;
then A128: (i + 1) + 1 >= ((len f) - 1) + 1 by XREAL_1:6;
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:233, XXREAL_0:2;
A132: ((len f) -' 1) + 1 = ((len f) - 1) + 1 by A5, XREAL_1:233, XXREAL_0:2
.= len f ;
then 1 + 1 <= ((len f) -' 1) + 1 by A2, TOPREAL1:def 8;
then A133: 1 <= (len f) -' 1 by XREAL_1:6;
A134: i + (1 + 1) = len f by A118, A128, XXREAL_0:1;
now :: thesis: for x being object holds not x in (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j))
(1 + 1) - 1 <= (len f) - 1 by A5, XREAL_1:9;
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:25;
A137: (LSeg (f,i)) /\ (LSeg (f,((len f) -' 1))) = {(f /. (i + 1))} by A2, A91, A131, A134, TOPREAL1:def 6;
f /. (len f) in LSeg (f,((len f) -' 1)) by A132, A133, TOPREAL1:21;
then A138: g . 1 in LSeg (f,((len f) -' 1)) by A1, A61, FINSEQ_4:15;
given x being object 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:15, NAT_1:11;
len f in dom f by A61, FINSEQ_3:25;
then len f = (len f) -' 1 by A2, A141, A136, FUNCT_1:def 4;
then len f = (len f) - 1 by A5, XREAL_1:233, 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 3;
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:9;
then (len f) + 1 <= (len f) + (len (mid (g,2,(len g)))) by A10, XREAL_1:7;
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 :: thesis: ( ( 1 <= i & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) or ( i < 1 & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) )
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:15;
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:15;
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:64;
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 3;
A152: 1 <= i + 1 by A147, NAT_D:48;
then A153: f /. (i + 1) = f . (i + 1) by A85, FINSEQ_4:15;
(f ^ (mid (g,2,(len g)))) /. (i + 1) = (f ^ (mid (g,2,(len g)))) . (i + 1) by A143, A152, FINSEQ_4:15;
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:64;
then LSeg ((f ^ (mid (g,2,(len g)))),i) = LSeg (f,i) by A85, A147, A151, TOPREAL1:def 3;
then A154: LSeg ((f ^ (mid (g,2,(len g)))),i) c= L~ f by TOPREAL3:19;
A155: j <= len (f ^ (mid (g,2,(len g)))) by A85, NAT_D:46;
A156: now :: thesis: ( 1 > j -' (len f) implies (f ^ (mid (g,2,(len g)))) . j = g . ((j -' (len f)) + 1) )
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:6;
then j - (len f) = 0 by A85, XREAL_1:233;
hence (f ^ (mid (g,2,(len g)))) . j = g . ((j -' (len f)) + 1) by A1, A61, A157, FINSEQ_1:64; :: 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:15;
A159: now :: thesis: ( 1 > (j + 1) -' (len f) implies (f ^ (mid (g,2,(len g)))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) )
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:6;
then (j + 1) - (len f) = 0 by A144, XREAL_1:233;
hence (f ^ (mid (g,2,(len g)))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) by A1, A61, A160, FINSEQ_1:64; :: thesis: verum
end;
(j + 1) + 1 <= ((len f) + ((len g) - 1)) + 1 by A6, A10, A85, XREAL_1:6;
then ((j + 1) + 1) - (len f) <= ((len f) + (len g)) - (len f) by XREAL_1:9;
then ((j - (len f)) + 1) + 1 <= len g ;
then A161: ((j -' (len f)) + 1) + 1 <= len g by A142, XREAL_1:233;
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:15, NAT_1:11;
(((j -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by A161, XREAL_1:9;
then A163: (j -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then (j -' (len f)) + 1 <= ((len g) -' 2) + 1 by A8, XREAL_1:233;
then A164: j -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;
A165: now :: thesis: ( 1 <= j -' (len f) implies (f ^ (mid (g,2,(len g)))) . j = g . ((j -' (len f)) + 1) )
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:6;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . j = (mid (g,2,(len g))) . (j -' (len f)) by A167, XREAL_1:233;
then (f ^ (mid (g,2,(len g)))) . j = g . (((j -' (len f)) + 2) - 1) by A8, A164, A166, FINSEQ_6:122;
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:233
.= (j + 1) - (len f)
.= (j + 1) -' (len f) by A144, XREAL_1:233 ;
A169: now :: thesis: ( 1 <= (j + 1) -' (len f) implies (f ^ (mid (g,2,(len g)))) . (j + 1) = g . (((j + 1) -' (len f)) + 1) )
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:6;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . (j + 1) = (mid (g,2,(len g))) . ((j + 1) -' (len f)) by A171, XREAL_1:233;
then (f ^ (mid (g,2,(len g)))) . (j + 1) = g . ((((j + 1) -' (len f)) + 2) - 1) by A8, A163, A168, A170, FINSEQ_6:122;
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 3;
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:15;
g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by A161, FINSEQ_4:15, 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 3;
then LSeg ((f ^ (mid (g,2,(len g)))),j) c= L~ g by TOPREAL3:19;
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 :: thesis: for x being object holds not x in (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j))
A176: 1 + 1 in dom g by A8, FINSEQ_3:25;
A177: (j -' (len f)) + 1 = (j - (len f)) + 1 by A142, XREAL_1:233;
A178: 1 + 1 <= len g by A3, TOPREAL1:def 8;
given x being object 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:15;
then x in LSeg (g,1) by A178, TOPREAL1:21;
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 7;
then 1 >= j -' (len f) by XREAL_1:6;
then 1 >= j - (len f) by NAT_D:39;
then A183: 1 + (len f) >= (j - (len f)) + (len f) by XREAL_1:6;
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 3;
then (LSeg (g,1)) /\ (LSeg (g,((j -' (len f)) + 1))) = {(g /. (1 + 1))} by A3, A184, A177, TOPREAL1:def 6;
then A185: x = g /. (1 + 1) by A182, TARSKI:def 1
.= g . (1 + 1) by A8, FINSEQ_4:15 ;
1 in dom g by A9, FINSEQ_3:25;
hence contradiction by A3, A181, A185, A176, FUNCT_1:def 4; :: 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 3;
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:233;
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:233, XXREAL_0:2;
(i + 1) - (len f) < j - (len f) by A63, XREAL_1:9;
then A198: ((i -' (len f)) + 1) + 1 < (j -' (len f)) + 1 by A188, A197, XREAL_1:6;
now :: thesis: ( ( j + 1 <= len (f ^ (mid (g,2,(len g)))) & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) or ( j + 1 > len (f ^ (mid (g,2,(len g)))) & (LSeg ((f ^ (mid (g,2,(len g)))),i)) /\ (LSeg ((f ^ (mid (g,2,(len g)))),j)) = {} ) )
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:15;
(len f) + 1 <= j by A194, NAT_1:13;
then A202: ((len f) + 1) - (len f) <= j - (len f) by XREAL_1:9;
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:22;
then A208: (i + 1) - (len f) < ((len f) + ((len g) - 1)) - (len f) by XREAL_1:9;
then A209: ((i - (len f)) + 1) + 1 < ((len g) - 1) + 1 by XREAL_1:6;
then ((i -' (len f)) + 1) + 1 <= len g by A187, XREAL_1:233;
then A210: g /. (((i -' (len f)) + 1) + 1) = g . (((i -' (len f)) + 1) + 1) by FINSEQ_4:15, 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:15;
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 3;
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 3;
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:15, NAT_1:11;
A216: now :: thesis: ( ( i <= len f & (f ^ (mid (g,2,(len g)))) /. i = g /. ((i -' (len f)) + 1) ) or ( i > len f & (f ^ (mid (g,2,(len g)))) /. i = g /. ((i -' (len f)) + 1) ) )
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:64
.= g . ((i -' (len f)) + 1) by A217, XREAL_1:232 ;
hence (f ^ (mid (g,2,(len g)))) /. i = g /. ((i -' (len f)) + 1) by A203, A207, A215, FINSEQ_4:15; :: 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:9;
((i -' (len f)) + 1) - 1 <= (len g) - 1 by A214, XREAL_1:9;
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, FINSEQ_6:108
.= g . (((i -' (len f)) + 2) - 1) by A8, A188, A219, A220, FINSEQ_6:122
.= g . ((i -' (len f)) + 1) ;
hence (f ^ (mid (g,2,(len g)))) /. i = g /. ((i -' (len f)) + 1) by A203, A207, A215, FINSEQ_4:15; :: thesis: verum
end;
end;
end;
j + 1 <= (len f) + ((len g) - 1) by A10, A199, FINSEQ_1:22;
then A221: (j + 1) - (len f) <= ((len f) + ((len g) - 1)) - (len f) by XREAL_1:9;
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, FINSEQ_6:108
.= g . (((j -' (len f)) + 1) + 1) by A8, A197, A193, A222, A223, FINSEQ_6:122 ;
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, FINSEQ_6:108
.= g . (((i -' (len f)) + 1) + 1) by A8, A188, A196, A226, A225, FINSEQ_6:122 ;
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 3;
A228: ((j - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by A221, XREAL_1:6;
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:15, 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:15;
((j -' (len f)) + 1) + 1 <= len g by A63, A186, A228, XREAL_1:233, XXREAL_0:2;
then A233: g /. (((j -' (len f)) + 1) + 1) = g . (((j -' (len f)) + 1) + 1) by FINSEQ_4:15, NAT_1:11;
((j -' (len f)) + 1) - 1 <= (len g) - 1 by A229, XREAL_1:9;
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, FINSEQ_6:108
.= g . (((j -' (len f)) + 2) - 1) by A8, A197, A202, A234, FINSEQ_6:122
.= 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 3;
then LSeg ((f ^ (mid (g,2,(len g)))),i) misses LSeg ((f ^ (mid (g,2,(len g)))),j) by A3, A198, A227, TOPREAL1:def 7;
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 3;
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 3;
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:22;
then (i + 1) + 1 <= (len f) + (((len g) -' 2) + 1) by A8, A9, FINSEQ_6:118;
then (i + 1) + 1 <= (len f) + (((len g) - (1 + 1)) + 1) by A8, XREAL_1:233;
then A242: ((i + 1) + 1) - (len f) <= ((len f) + (((len g) - (1 + 1)) + 1)) - (len f) by XREAL_1:9;
then A243: (((i + 1) - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by XREAL_1:6;
then A244: (((i - (len f)) + 1) + 1) + 1 <= len g ;
now :: thesis: ( ( i + 2 <= len f & (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))} ) or ( i + 2 > len f & (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))} ) )
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:15;
(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:15;
then A248: (f ^ (mid (g,2,(len g)))) /. (i + 1) = f /. (i + 1) by A238, A247, A246, FINSEQ_1:64;
A249: f /. ((i + 1) + 1) = f . ((i + 1) + 1) by A240, A245, FINSEQ_4:15;
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 3;
A251: (f ^ (mid (g,2,(len g)))) /. i = (f ^ (mid (g,2,(len g)))) . i by A236, A239, FINSEQ_4:15;
A252: i <= len f by A247, NAT_D:46;
then f /. i = f . i by A236, FINSEQ_4:15;
then A253: (f ^ (mid (g,2,(len g)))) /. i = f /. i by A236, A252, A251, FINSEQ_1:64;
(f ^ (mid (g,2,(len g)))) /. ((i + 1) + 1) = (f ^ (mid (g,2,(len g)))) . ((i + 1) + 1) by A237, A240, FINSEQ_4:15;
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:64;
then A254: LSeg ((f ^ (mid (g,2,(len g)))),(i + 1)) = LSeg (f,(i + 1)) by A238, A245, A250, TOPREAL1:def 3;
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 3;
then LSeg ((f ^ (mid (g,2,(len g)))),i) = LSeg (f,i) by A236, A247, A253, A248, TOPREAL1:def 3;
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 6; :: 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 :: thesis: ( ( i + 2 > (len f) + 1 & (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))} ) or ( i + 2 = (len f) + 1 & (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))} ) )
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:6;
A259: now :: thesis: ( 1 > i -' (len f) implies (f ^ (mid (g,2,(len g)))) . i = g . ((i -' (len f)) + 1) )
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:6;
then i - (len f) = 0 by A258, XREAL_1:233;
hence (f ^ (mid (g,2,(len g)))) . i = g . ((i -' (len f)) + 1) by A1, A61, A260, FINSEQ_1:64; :: thesis: verum
end;
A261: i + 1 >= len f by A257, NAT_D:48;
A262: now :: thesis: ( 1 > (i + 1) -' (len f) implies (f ^ (mid (g,2,(len g)))) . (i + 1) = g . (((i + 1) -' (len f)) + 1) )
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:6;
then (i + 1) - (len f) = 0 by A261, XREAL_1:233;
hence (f ^ (mid (g,2,(len g)))) . (i + 1) = g . (((i + 1) -' (len f)) + 1) by A1, A61, A263, FINSEQ_1:64; :: 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:9;
then (i - (len f)) + 1 >= 1 ;
then A264: (i -' (len f)) + 1 >= 1 by A258, XREAL_1:233;
then A265: ((i -' (len f)) + 1) + 1 >= 1 by NAT_D:48;
then A266: ((i - (len f)) + 1) + 1 >= 1 by A258, XREAL_1:233;
then ((i + 1) - (len f)) + 1 >= 1 ;
then A267: ((i + 1) -' (len f)) + 1 >= 1 by A261, XREAL_1:233;
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:6;
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:15;
(((i + 1) -' (len f)) + 1) + 1 <= len g by A243, A261, XREAL_1:233;
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 3;
(((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:233;
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 3;
(((i -' (len f)) + 1) + 1) - 1 <= (len g) - 1 by A274, XREAL_1:9;
then (i -' (len f)) + 1 <= ((len g) - 2) + 1 ;
then A276: (i -' (len f)) + 1 <= ((len g) -' 2) + 1 by A8, XREAL_1:233;
then A277: i -' (len f) <= ((len g) -' 2) + 1 by NAT_D:46;
A278: now :: thesis: ( 1 <= i -' (len f) implies (f ^ (mid (g,2,(len g)))) . i = g . ((i -' (len f)) + 1) )
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:6;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . i = (mid (g,2,(len g))) . (i -' (len f)) by A280, XREAL_1:233;
then (f ^ (mid (g,2,(len g)))) . i = g . (((i -' (len f)) + 2) - 1) by A8, A277, A279, FINSEQ_6:122;
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:15;
then A281: (f ^ (mid (g,2,(len g)))) /. i = g /. ((i -' (len f)) + 1) by A236, A239, A278, A259, FINSEQ_4:15;
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:15;
(i - (len f)) + 1 <= ((len g) -' 2) + 1 by A258, A276, XREAL_1:233;
then (i + 1) - (len f) <= ((len g) -' 2) + 1 ;
then A284: (i + 1) -' (len f) <= ((len g) -' 2) + 1 by A261, XREAL_1:233;
A285: now :: thesis: ( 1 <= (i + 1) -' (len f) implies (f ^ (mid (g,2,(len g)))) . (i + 1) = g . (((i + 1) -' (len f)) + 1) )
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:6;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . (i + 1) = (mid (g,2,(len g))) . ((i + 1) -' (len f)) by A287, XREAL_1:233;
then (f ^ (mid (g,2,(len g)))) . (i + 1) = g . ((((i + 1) -' (len f)) + 2) - 1) by A8, A284, A286, FINSEQ_6:122;
hence (f ^ (mid (g,2,(len g)))) . (i + 1) = g . (((i + 1) -' (len f)) + 1) ; :: thesis: verum
end;
A288: now :: thesis: ( 1 > ((i + 1) + 1) -' (len f) implies (f ^ (mid (g,2,(len g)))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1) )
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:6;
then A290: ((i + 1) + 1) - (len f) = 0 by A266, XREAL_0:def 2;
((i + 1) + 1) -' (len f) = 0 by A289, XREAL_1:6;
hence (f ^ (mid (g,2,(len g)))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1) by A1, A61, A290, FINSEQ_1:64; :: 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:233;
then A292: ((i + 1) -' (len f)) + 1 = ((i -' (len f)) + 1) + 1 by A261, XREAL_1:233;
A293: ((i + 1) + 1) -' (len f) <= ((len g) - 2) + 1 by A242, A266, XREAL_0:def 2;
A294: now :: thesis: ( 1 <= ((i + 1) + 1) -' (len f) implies (f ^ (mid (g,2,(len g)))) . ((i + 1) + 1) = g . ((((i + 1) + 1) -' (len f)) + 1) )
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:6;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . ((i + 1) + 1) = (mid (g,2,(len g))) . (((i + 1) + 1) -' (len f)) by A296, XREAL_1:233;
then (f ^ (mid (g,2,(len g)))) . ((i + 1) + 1) = g . (((((i + 1) + 1) -' (len f)) + 2) - 1) by A8, A293, A295, FINSEQ_6:122;
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:15;
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 3;
A299: (f ^ (mid (g,2,(len g)))) /. (i + 1) = (f ^ (mid (g,2,(len g)))) . (i + 1) by A238, A241, FINSEQ_4:15;
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 3;
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 6; :: 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:15;
then A302: f /. (i + 1) = g /. 1 by A1, A9, A300, FINSEQ_4:15;
(f ^ (mid (g,2,(len g)))) /. (i + 1) = (f ^ (mid (g,2,(len g)))) . (i + 1) by A238, A241, FINSEQ_4:15;
then A303: (f ^ (mid (g,2,(len g)))) /. (i + 1) = f /. (i + 1) by A238, A300, A301, FINSEQ_1:64;
A304: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A236, A300, TOPREAL1:def 3;
A305: (f ^ (mid (g,2,(len g)))) /. i = (f ^ (mid (g,2,(len g)))) . i by A236, A239, FINSEQ_4:15;
(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:15;
then A307: (f ^ (mid (g,2,(len g)))) /. i = f /. i by A236, A306, A305, FINSEQ_1:64;
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 3;
i = (len f) - 1 by A300;
then A309: i = (len f) -' 1 by A5, XREAL_1:233, XXREAL_0:2;
A310: g /. 1 in LSeg ((g /. 1),(g /. (1 + 1))) by RLTOPSP1:68;
A311: g /. 1 = g . 1 by A9, FINSEQ_4:15;
then g /. 1 = f /. (len f) by A1, A61, FINSEQ_4:15;
then A312: g /. 1 in LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by RLTOPSP1:68;
(len g) - 2 >= 0 by A8, XREAL_1:48;
then A313: 0 + 1 <= ((len g) - 2) + 1 by XREAL_1:6;
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, FINSEQ_6:108;
then A314: (f ^ (mid (g,2,(len g)))) . ((i + 1) + 1) = g . ((2 + 1) -' 1) by A8, A300, A313, FINSEQ_6:122
.= g . 2 by NAT_D:34 ;
A315: LSeg (g,1) c= L~ g by TOPREAL3:19;
LSeg (f,i) c= L~ f by TOPREAL3:19;
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:232
.= 1 ;
then A318: g /. ((((i + 1) -' (len f)) + 1) + 1) = g . ((((i + 1) -' (len f)) + 1) + 1) by A8, FINSEQ_4:15;
LSeg (g,1) = LSeg ((g /. 1),(g /. (1 + 1))) by A8, TOPREAL1:def 3;
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:31;
A320: (f ^ (mid (g,2,(len g)))) /. ((i + 1) + 1) = (f ^ (mid (g,2,(len g)))) . ((i + 1) + 1) by A237, A240, FINSEQ_4:15;
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 3;
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 3;
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 :: thesis: ( ( i < len f & ( ((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 ) ) or ( i >= len f & ( ((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 ) ) )
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:15;
f /. i = f . i by A322, A324, FINSEQ_4:15;
then A326: (f ^ (mid (g,2,(len g)))) /. i = f /. i by A322, A324, A325, FINSEQ_1:64;
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:15;
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:64;
f /. (i + 1) = f . (i + 1) by A327, A329, FINSEQ_4:15;
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 5; :: 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:233;
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:48;
then A335: i -' (len f) = i - (len f) by XREAL_0:def 2;
A336: now :: thesis: ( 1 > i -' (len f) implies (f ^ (mid (g,2,(len g)))) . i = g . ((i -' (len f)) + 1) )
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:6;
hence (f ^ (mid (g,2,(len g)))) . i = g . ((i -' (len f)) + 1) by A1, A61, A335, FINSEQ_1:64; :: 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:233
.= ((i - (len f)) + 1) + 1
.= ((i -' (len f)) + 1) + 1 by A331, XREAL_1:233 ;
A339: (i + 1) - (len f) <= ((len f) + ((len g) - 1)) - (len f) by A6, A10, A323, XREAL_1:9;
then A340: ((i - (len f)) + 1) + 1 <= ((len g) - 1) + 1 by XREAL_1:6;
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 :: thesis: ( 1 <= i -' (len f) implies (f ^ (mid (g,2,(len g)))) . i = g . ((i -' (len f)) + 1) )
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:6;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . i = (mid (g,2,(len g))) . (i -' (len f)) by A345, XREAL_1:233;
then (f ^ (mid (g,2,(len g)))) . i = g . (((i -' (len f)) + 2) - 1) by A8, A342, A344, FINSEQ_6:122;
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:15;
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:233;
then A348: (i + 1) -' (len f) <= ((len g) -' 2) + 1 by A337, XREAL_1:233;
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, FINSEQ_6:108;
then (f ^ (mid (g,2,(len g)))) . (i + 1) = (mid (g,2,(len g))) . ((i + 1) -' (len f)) by A337, XREAL_1:233;
then A349: (f ^ (mid (g,2,(len g)))) . (i + 1) = g . ((((i + 1) -' (len f)) + 2) - 1) by A8, A348, A332, FINSEQ_6:122;
((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:15, 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:15, NAT_1:11;
then (f ^ (mid (g,2,(len g)))) /. i = g /. ((i -' (len f)) + 1) by A322, A333, A343, A336, FINSEQ_4:15;
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 5; :: 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 5, TOPREAL1:def 6, TOPREAL1:def 7;
hence f ^ (mid (g,2,(len g))) is being_S-Seq by A60, A7, TOPREAL1:def 8; :: thesis: verum