let f be constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 > i2 holds
( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) )
let g be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 > i2 holds
( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) )
let i1, i2 be Nat; :: thesis: ( g is_a_part>_of f,i1,i2 & i1 > i2 implies ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) ) )
assume that
A1: g is_a_part>_of f,i1,i2 and
A2: i1 > i2 ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) )
A3: 1 <= len g by A1;
A4: f . i2 = f . (S_Drop (((i1 + (len g)) -' 1),f)) by A1;
A5: i2 <= i2 + 1 by NAT_1:11;
A6: i1 <= i1 + 1 by NAT_1:12;
A7: 1 <= i1 by A1;
A8: i1 + 1 <= len f by A1;
then A9: (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A10: 1 <= (len f) - 1 by A7, XXREAL_0:2;
then A11: (len f) - 1 = (len f) -' 1 by NAT_D:39;

A12: now :: thesis: ( ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 & S_Drop (((i1 + (len g)) -' 1),f) < len f ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & S_Drop (((i1 + (len g)) -' 1),f) < len f ) )

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

case A13: ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis: S_Drop (((i1 + (len g)) -' 1),f) < len f

A14: i1 <= (len f) -' 1 by A8, NAT_D:49;
then A15: ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 by A7, NAT_D:1;
1 <= (len f) -' 1 by A7, A14, XXREAL_0:2;
then A16: (len f) -' 1 < len f by NAT_D:51;
S_Drop (((i1 + (len g)) -' 1),f) = ((i1 + (len g)) -' 1) mod ((len f) -' 1) by A13, Def1;
hence S_Drop (((i1 + (len g)) -' 1),f) < len f by A15, A16, XXREAL_0:2; :: thesis: verum

end;

case A17: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis: S_Drop (((i1 + (len g)) -' 1),f) < len f

i1 <= (len f) -' 1 by A8, NAT_D:49;
then A18: 1 <= (len f) -' 1 by A7, XXREAL_0:2;
S_Drop (((i1 + (len g)) -' 1),f) = (len f) -' 1 by A17, Def1;
hence S_Drop (((i1 + (len g)) -' 1),f) < len f by A18, NAT_D:51; :: thesis: verum

end;

end;

end;

i1 <= (len f) -' 1 by A8, NAT_D:49;
then 1 <= (len f) -' 1 by A7, XXREAL_0:2;
then A19: (len f) -' 1 < len f by NAT_D:51;

A20: now :: thesis: ( ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 & 1 <= S_Drop (((i1 + (len g)) -' 1),f) ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & 1 <= S_Drop (((i1 + (len g)) -' 1),f) ) )

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

case ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis: 1 <= S_Drop (((i1 + (len g)) -' 1),f)

then 0 + 1 <= ((i1 + (len g)) -' 1) mod ((len f) -' 1) by NAT_1:13;
hence 1 <= S_Drop (((i1 + (len g)) -' 1),f) by Def1; :: thesis: verum

end;

case A21: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis: 1 <= S_Drop (((i1 + (len g)) -' 1),f)

A22: i1 <= (len f) -' 1 by A8, NAT_D:49;
S_Drop (((i1 + (len g)) -' 1),f) = (len f) -' 1 by A21, Def1;
hence 1 <= S_Drop (((i1 + (len g)) -' 1),f) by A7, A22, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A23: 1 <= i2 by A1;
A24: i2 + 1 <= len f by A1;
then A25: i2 <= (len f) -' 1 by NAT_D:49;
then A26: 1 <= (len f) -' 1 by A23, XXREAL_0:2;
then (len f) -' 1 < len f by NAT_D:51;
then A27: i2 < len f by A25, XXREAL_0:2;
A28: len g < len f by A1;
A29: 0 <> (len f) -' 1 by A10, NAT_D:39;

now :: thesis: ( ( i2 < S_Drop (((i1 + (len g)) -' 1),f) & contradiction ) or ( i2 > S_Drop (((i1 + (len g)) -' 1),f) & contradiction ) or ( i2 = S_Drop (((i1 + (len g)) -' 1),f) & len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) )

per cases ( i2 < S_Drop (((i1 + (len g)) -' 1),f) or i2 > S_Drop (((i1 + (len g)) -' 1),f) or i2 = S_Drop (((i1 + (len g)) -' 1),f) ) by XXREAL_0:1;

case A30: i2 < S_Drop (((i1 + (len g)) -' 1),f) ; :: thesis: contradiction

i2 <= len f by A24, NAT_D:46;
then A31: f /. i2 = f . i2 by A23, FINSEQ_4:15;
A32: 1 <= S_Drop (((i1 + (len g)) -' 1),f) by A23, A30, XXREAL_0:2;
f /. i2 <> f /. (S_Drop (((i1 + (len g)) -' 1),f)) by A23, A12, A30, GOBOARD7:36;
hence contradiction by A4, A12, A31, A32, FINSEQ_4:15; :: thesis: verum

end;

case A33: i2 > S_Drop (((i1 + (len g)) -' 1),f) ; :: thesis: contradiction

i2 <= len f by A24, NAT_D:46;
then A34: f /. i2 = f . i2 by A23, FINSEQ_4:15;
f /. i2 <> f /. (S_Drop (((i1 + (len g)) -' 1),f)) by A20, A27, A33, GOBOARD7:36;
hence contradiction by A4, A20, A12, A34, FINSEQ_4:15; :: thesis: verum

end;

case A35: i2 = S_Drop (((i1 + (len g)) -' 1),f) ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) )

now :: thesis: ( ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 & len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & contradiction ) )

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

case A36: ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) )

( ex n being Nat st
( (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) & ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & (len f) -' 1 = 0 ) ) by NAT_D:def 2;
then consider n being Nat such that
A37: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) by A10, NAT_D:39;
A38: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + i2 by A35, A36, A37, Def1;

now :: thesis: ( ( n = 0 & contradiction ) or ( n <> 0 & len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) )

per cases ( n = 0 or n <> 0 ) ;

case n = 0 ; :: thesis: contradiction

then i2 = (i1 + (len g)) -' 1 by A35, A36, A37, Def1;
then i2 + 1 = ((i1 + (len g)) - 1) + 1 by A23, NAT_D:39
.= i1 + (len g) ;
hence contradiction by A2, A3, XREAL_1:8; :: thesis: verum

end;

case n <> 0 ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) )

then A39: 0 + 1 <= n by NAT_1:13;

now :: thesis: ( ( 1 = n & len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) or ( 1 < n & contradiction ) )

per cases ( 1 = n or 1 < n ) by A39, XXREAL_0:1;

case A40: 1 = n ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) )

(len f) -' 1 = (len f) - 1 by A26, NAT_D:39;
then A41: (i1 + (len g)) - 1 = ((len f) - 1) + i2 by A7, A38, A40, NAT_D:37;
then A42: len g = ((len f) + i2) - i1 ;
A43: (len f) -' 1 <= len f by NAT_D:50;
A44: dom g = Seg (len g) by FINSEQ_1:def 3;
A45: i1 <= len f by A8, A6, XXREAL_0:2;
A46: 1 <= (len f) -' 1 by A10, NAT_D:39;
A47: i1 <= (len f) -' 1 by A9, A10, NAT_D:39;
then A48: len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1 by A7, A45, A46, A43, FINSEQ_6:118;
A49: (((len f) -' 1) -' i1) + 1 = (((len f) - 1) - i1) + 1 by A9, A11, XREAL_1:233
.= (len f) - i1 ;
len ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) = (len (mid (f,i1,((len f) -' 1)))) + (len (f | i2)) by FINSEQ_1:22;
then len ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) = ((len f) - i1) + i2 by A24, A5, A48, A49, FINSEQ_1:59, XXREAL_0:2
.= ((len f) + i2) - i1
.= ((len f) + i2) -' i1 by A8, A6, NAT_D:37, XXREAL_0:2 ;
then A50: len ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) = len g by A8, A6, A42, NAT_D:37, XXREAL_0:2;
A51: ((len f) -' 1) -' i1 = ((len f) -' 1) - i1 by A9, A11, XREAL_1:233;
for j being Nat st j in dom g holds
g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j

proof

let j be Nat; :: thesis: ( j in dom g implies g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j )
assume A52: j in dom g ; :: thesis: g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j
then A53: 1 <= j by A44, FINSEQ_1:1;
then A54: (i1 + j) -' 1 = (i1 + j) - 1 by NAT_D:37;
i1 + j >= 1 + 1 by A7, A53, XREAL_1:7;
then A55: (i1 + j) -' 1 <> 0 by A54;
A56: j <= len g by A44, A52, FINSEQ_1:1;
then A57: g . j = f . (S_Drop (((i1 + j) -' 1),f)) by A1, A53;

now :: thesis: ( ( j <= len (mid (f,i1,((len f) -' 1))) & g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j ) or ( j > len (mid (f,i1,((len f) -' 1))) & g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j ) )

per cases ( j <= len (mid (f,i1,((len f) -' 1))) or j > len (mid (f,i1,((len f) -' 1))) ) ;

case A58: j <= len (mid (f,i1,((len f) -' 1))) ; :: thesis: g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j

then A59: j + i1 <= ((((len f) -' 1) - i1) + 1) + i1 by A48, A51, XREAL_1:6;

A60: now :: thesis: ( ( i1 + j = len f & S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 ) or ( i1 + j <> len f & S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 ) )

per cases ( i1 + j = len f or i1 + j <> len f ) ;

case A61: i1 + j = len f ; :: thesis: S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1

then ((i1 + j) -' 1) mod ((len f) -' 1) = 0 by NAT_D:25;
hence S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 by A61, Def1; :: thesis: verum

end;

case i1 + j <> len f ; :: thesis: S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1

then i1 + j < len f by A11, A59, XXREAL_0:1;
then (i1 + j) - 1 < (len f) - 1 by XREAL_1:9;
then A62: (i1 + j) -' 1 < (len f) -' 1 by A7, A11, NAT_D:37;
then ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 by A55, NAT_D:24;
then S_Drop (((i1 + j) -' 1),f) = ((i1 + j) -' 1) mod ((len f) -' 1) by Def1;
hence S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 by A62, NAT_D:24; :: thesis: verum

end;

end;

end;

A63: (len f) -' 1 <= len f by NAT_D:50;
j in dom (mid (f,i1,((len f) -' 1))) by A53, A58, FINSEQ_3:25;
then A64: ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j = (mid (f,i1,((len f) -' 1))) . j by FINSEQ_1:def 7;
A65: 1 <= j by A44, A52, FINSEQ_1:1;
i1 <= (len f) -' 1 by A9, A10, NAT_D:39;
hence g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j by A7, A45, A46, A57, A58, A64, A63, A65, A60, FINSEQ_6:118; :: thesis: verum

end;

case A66: j > len (mid (f,i1,((len f) -' 1))) ; :: thesis: g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j

j <= ((len f) + i2) - i1 by A41, A44, A52, FINSEQ_1:1;
then j + i1 <= (((len f) + i2) - i1) + i1 by XREAL_1:6;
then A67: (j + i1) - (len f) <= ((len f) + i2) - (len f) by XREAL_1:9;
j < len f by A28, A56, XXREAL_0:2;
then A68: j <= (len f) - 1 by SPPOL_1:1;
(i1 + 1) - 1 <= (len f) - 1 by A8, XREAL_1:9;
then A69: i1 + j <= ((len f) -' 1) + ((len f) -' 1) by A11, A68, XREAL_1:7;
A70: ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j = (f | i2) . (j - (len (mid (f,i1,((len f) -' 1))))) by A50, A56, A66, FINSEQ_6:108;
A71: (i1 + j) - 1 = (i1 + j) -' 1 by A7, NAT_D:37;
(len (mid (f,i1,((len f) -' 1)))) + 1 <= j by A66, NAT_1:13;
then ((len (mid (f,i1,((len f) -' 1)))) + 1) - (len (mid (f,i1,((len f) -' 1)))) <= j - (len (mid (f,i1,((len f) -' 1)))) by XREAL_1:9;
then 1 + (len f) <= ((i1 + j) - (len f)) + (len f) by A48, A49, XREAL_1:6;
then (1 + (len f)) - 1 <= (i1 + j) - 1 by XREAL_1:9;
then A72: (len f) -' 1 < (i1 + j) -' 1 by A19, A71, XXREAL_0:2;
j + i1 > ((len f) - i1) + i1 by A48, A49, A66, XREAL_1:6;
then A73: (i1 + j) - (len f) > (len f) - (len f) by XREAL_1:9;
then A74: (i1 + j) -' (len f) = (i1 + j) - (len f) by XREAL_0:def 2;
j - (len (mid (f,i1,((len f) -' 1)))) = j - ((len f) - i1) by A7, A45, A46, A43, A47, A49, FINSEQ_6:118
.= (j + i1) - (len f) ;
then A75: (f | i2) . (j - (len (mid (f,i1,((len f) -' 1))))) = f . ((i1 + j) -' (len f)) by A74, A67, FINSEQ_3:112;
i1 + j < (i1 + j) + 1 by NAT_1:13;
then (i1 + j) - 1 < ((i1 + j) + 1) - 1 by XREAL_1:9;
then A76: (i1 + j) -' 1 < ((len f) -' 1) + ((len f) -' 1) by A71, A69, XXREAL_0:2;

now :: thesis: ( ( ((i1 + j) -' 1) mod ((len f) -' 1) = 0 & contradiction ) or ( ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 & g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j ) )

per cases ( ((i1 + j) -' 1) mod ((len f) -' 1) = 0 or ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 ) ;

case ((i1 + j) -' 1) mod ((len f) -' 1) = 0 ; :: thesis: contradiction

hence contradiction by A72, A76, Th1; :: thesis: verum

end;

case A77: ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis: g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j

((i1 + j) -' (len f)) + ((len f) -' 1) = ((i1 + j) -' (len f)) + ((len f) - 1) by A10, NAT_D:39
.= ((i1 + j) - (len f)) + ((len f) - 1) by A73, XREAL_0:def 2
.= (i1 + j) - 1
.= (i1 + j) -' 1 by A53, NAT_D:37 ;
then A78: ((i1 + j) -' 1) mod ((len f) -' 1) = (((i1 + j) -' (len f)) + (((len f) -' 1) mod ((len f) -' 1))) mod ((len f) -' 1) by NAT_D:23
.= (((i1 + j) -' (len f)) + 0) mod ((len f) -' 1) by NAT_D:25
.= ((i1 + j) -' (len f)) mod ((len f) -' 1) ;
(i1 + j) - ((len f) -' 1) <= (((len f) -' 1) + ((len f) -' 1)) - ((len f) -' 1) by A69, XREAL_1:9;
then (i1 + j) - ((len f) - 1) <= (len f) -' 1 by A10, NAT_D:39;
then ((i1 + j) -' (len f)) + 1 <= (len f) -' 1 by A74;
then A79: (i1 + j) -' (len f) < (len f) -' 1 by NAT_1:13;
S_Drop (((i1 + j) -' 1),f) = ((i1 + j) -' 1) mod ((len f) -' 1) by A77, Def1;
hence g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j by A57, A70, A75, A78, A79, NAT_D:24; :: thesis: verum

end;

end;

end;

hence g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j ; :: thesis: verum

end;

end;

end;

hence g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j ; :: thesis: verum

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) by A8, A6, A42, A50, FINSEQ_2:9, NAT_D:37, XXREAL_0:2; :: thesis: verum

end;

case 1 < n ; :: thesis: contradiction

then 1 + 1 <= n by NAT_1:13;
then ((len f) -' 1) * n >= ((len f) -' 1) * (1 + 1) by XREAL_1:64;
then A80: (i1 + (len g)) -' 1 >= (((len f) -' 1) * (1 + 1)) + i2 by A38, XREAL_1:6;
A81: ((len f) -' 1) * (1 + 1) <= (((len f) -' 1) * (1 + 1)) + i2 by NAT_1:11;
A82: (i1 + 1) - 1 <= (len f) - 1 by A8, XREAL_1:9;
(len g) - 1 < (len f) -' 1 by A28, A11, XREAL_1:9;
then A83: i1 + ((len g) - 1) < ((len f) -' 1) + ((len f) -' 1) by A11, A82, XREAL_1:8;
(i1 + (len g)) - 1 = (i1 + (len g)) -' 1 by A7, NAT_D:37;
hence contradiction by A80, A83, A81, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) ; :: thesis: verum

end;

end;

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) ; :: thesis: verum

end;

case A84: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis: contradiction

ex n being Nat st
( (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) & ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 ) by A29, NAT_D:def 2;
then consider n being Nat such that
A85: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) ;

A86: now :: thesis: not n > 1

assume n > 1 ; :: thesis: contradiction
then n >= 1 + 1 by NAT_1:13;
then A87: (i1 + (len g)) -' 1 >= ((len f) -' 1) * (1 + 1) by A84, A85, NAT_1:4;
(len g) - 1 < (len f) - 1 by A28, XREAL_1:9;
then i1 + ((len g) - 1) < ((len f) -' 1) + ((len f) -' 1) by A9, A11, XREAL_1:8;
then (i1 + (len g)) - 1 < ((len f) -' 1) + ((len f) -' 1) ;
hence contradiction by A7, A87, NAT_1:12, XREAL_1:233; :: thesis: verum

end;

now :: thesis: not n = 0

assume n = 0 ; :: thesis: contradiction
then A88: i1 + (len g) <= 1 by A84, A85, NAT_D:36;
i1 + (len g) >= 1 + 1 by A7, A3, XREAL_1:7;
hence contradiction by A88, XXREAL_0:2; :: thesis: verum

end;

then n >= 0 + 1 by NAT_1:13;
then n = 1 by A86, XXREAL_0:1;
then (i1 + (len g)) -' 1 = i2 by A35, A84, A85, Def1;
then A89: (i1 + (len g)) - 1 = i2 by A23, NAT_D:39;
i2 - i2 < i1 - i2 by A2, XREAL_1:9;
then A90: - 0 > - (i1 - i2) by XREAL_1:24;
1 - 1 <= (len g) - 1 by A3, XREAL_1:9;
hence contradiction by A89, A90; :: thesis: verum

end;

end;

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) ; :: thesis: verum

end;

end;

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) ) by A23, FINSEQ_6:116; :: thesis: verum