let f be non constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 & i1 >= i2 holds
( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
let g be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 & i1 >= i2 holds
( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
let i1, i2 be Element of NAT ; :: thesis: ( g is_a_part<_of f,i1,i2 & i1 >= i2 implies ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) )
assume that
A1: g is_a_part<_of f,i1,i2 and
A2: i1 >= i2 ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
A3: 1 <= len g by A1, Def3;
g . (len g) = f . i2 by A1, Def3;
then A4: f . i2 = f . (S_Drop ((((len f) + i1) -' (len g)),f)) by A1, A3, Def3;
A5: i1 + 1 <= len f by A1, Def3;
i1 <= i1 + 1 by NAT_1:11;
then A6: i1 <= len f by A5, XXREAL_0:2;
A7: 1 <= i2 by A1, Def3;
A8: i2 + 1 <= len f by A1, Def3;
then (i2 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A9: 1 <= (len f) - 1 by A7, XXREAL_0:2;
then A10: (len f) - 1 = (len f) -' 1 by NAT_D:39;
A11: now
per cases ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 or (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ) ;
case A12: (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 ; :: thesis: S_Drop ((((len f) + i1) -' (len g)),f) < len f
A13: i2 <= (len f) -' 1 by A8, NAT_D:49;
then A14: (((len f) + i1) -' (len g)) mod ((len f) -' 1) < (len f) -' 1 by A7, NAT_D:1;
1 <= (len f) -' 1 by A7, A13, XXREAL_0:2;
then A15: (len f) -' 1 < len f by NAT_D:51;
S_Drop ((((len f) + i1) -' (len g)),f) = (((len f) + i1) -' (len g)) mod ((len f) -' 1) by A12, Def1;
hence S_Drop ((((len f) + i1) -' (len g)),f) < len f by A14, A15, XXREAL_0:2; :: thesis: verum
end;
case A16: (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ; :: thesis: S_Drop ((((len f) + i1) -' (len g)),f) < len f
i2 <= (len f) -' 1 by A8, NAT_D:49;
then A17: 1 <= (len f) -' 1 by A7, XXREAL_0:2;
S_Drop ((((len f) + i1) -' (len g)),f) = (len f) -' 1 by A16, Def1;
hence S_Drop ((((len f) + i1) -' (len g)),f) < len f by A17, NAT_D:51; :: thesis: verum
end;
end;
end;
A18: i2 <= (len f) -' 1 by A8, NAT_D:49;
then 1 <= (len f) -' 1 by A7, XXREAL_0:2;
then (len f) -' 1 < len f by NAT_D:51;
then A19: i2 < len f by A18, XXREAL_0:2;
A20: 0 <> (len f) -' 1 by A9, NAT_D:39;
A21: now
per cases ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 or (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ) ;
case (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 ; :: thesis: 1 <= S_Drop ((((len f) + i1) -' (len g)),f)
then 0 + 1 <= (((len f) + i1) -' (len g)) mod ((len f) -' 1) by NAT_1:13;
hence 1 <= S_Drop ((((len f) + i1) -' (len g)),f) by Def1; :: thesis: verum
end;
case A22: (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ; :: thesis: 1 <= S_Drop ((((len f) + i1) -' (len g)),f)
A23: i2 <= (len f) -' 1 by A8, NAT_D:49;
S_Drop ((((len f) + i1) -' (len g)),f) = (len f) -' 1 by A22, Def1;
hence 1 <= S_Drop ((((len f) + i1) -' (len g)),f) by A7, A23, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A24: len g < len f by A1, Def3;
A25: 0 < (len f) -' 1 by A9, NAT_D:39;
now
per cases ( i2 < S_Drop ((((len f) + i1) -' (len g)),f) or i2 > S_Drop ((((len f) + i1) -' (len g)),f) or i2 = S_Drop ((((len f) + i1) -' (len g)),f) ) by XXREAL_0:1;
case A26: i2 < S_Drop ((((len f) + i1) -' (len g)),f) ; :: thesis: contradiction
i2 <= len f by A8, NAT_1:13;
then A27: f /. i2 = f . i2 by A7, FINSEQ_4:15;
A28: 1 <= S_Drop ((((len f) + i1) -' (len g)),f) by A7, A26, XXREAL_0:2;
f /. i2 <> f /. (S_Drop ((((len f) + i1) -' (len g)),f)) by A7, A11, A26, GOBOARD7:36;
hence contradiction by A4, A11, A27, A28, FINSEQ_4:15; :: thesis: verum
end;
case A29: i2 > S_Drop ((((len f) + i1) -' (len g)),f) ; :: thesis: contradiction
i2 <= len f by A8, NAT_1:13;
then A30: f /. i2 = f . i2 by A7, FINSEQ_4:15;
f /. i2 <> f /. (S_Drop ((((len f) + i1) -' (len g)),f)) by A21, A19, A29, GOBOARD7:36;
hence contradiction by A4, A21, A11, A30, FINSEQ_4:15; :: thesis: verum
end;
case A31: i2 = S_Drop ((((len f) + i1) -' (len g)),f) ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
now
per cases ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 or (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ) ;
case A32: (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
ex n being Nat st
( ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) & (((len f) + i1) -' (len g)) mod ((len f) -' 1) < (len f) -' 1 ) by A20, NAT_D:def 2;
then consider n being Nat such that
A33: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) ;
A34: ( n = 0 or n >= 0 + 1 ) by NAT_1:13;
A35: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + i2 by A31, A32, A33, Def1;
now
per cases ( n = 0 or n = 1 or n > 1 ) by A34, XXREAL_0:1;
case n = 0 ; :: thesis: contradiction
then i2 = ((len f) + i1) -' (len g) by A31, A32, A33, Def1;
then i2 = ((len f) + i1) - (len g) by A24, NAT_D:37;
then i2 + (len g) = i1 + (len f) ;
hence contradiction by A2, A24, XREAL_1:8; :: thesis: verum
end;
case A36: n = 1 ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
A37: ((len f) + i1) -' (len g) = ((len f) + i1) - (len g) by A24, NAT_D:37;
A38: ((len f) - 1) + i2 = ((len f) + i1) -' (len g) by A10, A31, A32, A33, A36, Def1;
then A39: len g = (i1 - i2) + 1 by A37;
then A40: len g = (i1 -' i2) + 1 by A2, XREAL_1:233;
A41: dom g = Seg (len g) by FINSEQ_1:def 3;
A42: for j being Nat st j in dom g holds
g . j = (mid (f,i1,i2)) . j
proof
let j be Nat; :: thesis: ( j in dom g implies g . j = (mid (f,i1,i2)) . j )
A43: j in NAT by ORDINAL1:def 12;
assume A44: j in dom g ; :: thesis: g . j = (mid (f,i1,i2)) . j
then A45: 1 <= j by A41, FINSEQ_1:1;
A46: j <= len g by A41, A44, FINSEQ_1:1;
1 - 1 <= i2 - 1 by A7, XREAL_1:9;
then A47: i1 - 0 >= i1 - (i2 - 1) by XREAL_1:10;
then A48: (i1 -' j) + 1 = (i1 - j) + 1 by A38, A37, A46, XREAL_1:233, XXREAL_0:2;
A49: j <= i1 by A38, A37, A46, A47, XXREAL_0:2;
A50: now
per cases ( ((len f) + i1) -' j = (len f) -' 1 or ((len f) + i1) -' j <> (len f) -' 1 ) ;
case ((len f) + i1) -' j = (len f) -' 1 ; :: thesis: contradiction
then ((len f) + i1) - j = (len f) -' 1 by A24, A46, NAT_D:37, XXREAL_0:2
.= (len f) - 1 by A9, NAT_D:39 ;
then i1 - j = - 1 ;
hence contradiction by A49, XREAL_1:48; :: thesis: verum
end;
case ((len f) + i1) -' j <> (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
(i1 + 1) + 0 < (len f) + j by A5, A45, XREAL_1:8;
then (i1 + 1) - j < ((len f) + j) - j by XREAL_1:9;
then ((i1 + 1) - j) - 1 < (len f) - 1 by XREAL_1:9;
then i1 - j < (len f) - 1 ;
then i1 -' j < (len f) -' 1 by A10, A38, A37, A46, A47, XREAL_1:233, XXREAL_0:2;
then A51: (i1 -' j) + 1 <= (len f) -' 1 by NAT_1:13;
A52: ((len f) + i1) -' j = ((len f) + i1) - j by A24, A46, NAT_D:37, XXREAL_0:2;
now
per cases ( (i1 -' j) + 1 = (len f) -' 1 or (i1 -' j) + 1 < (len f) -' 1 ) by A51, XXREAL_0:1;
case A53: (i1 -' j) + 1 = (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
((len f) + i1) -' j = ((((len f) - 1) + 1) + i1) - j by A24, A46, NAT_D:37, XXREAL_0:2
.= ((len f) -' 1) + ((i1 - j) + 1) by A10
.= ((len f) -' 1) + ((len f) -' 1) by A38, A37, A46, A47, A53, XREAL_1:233, XXREAL_0:2 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = 0 by Th8;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 by A53, Def1; :: thesis: verum
end;
case A54: (i1 -' j) + 1 < (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
A55: len f = ((len f) - 1) + 1
.= ((len f) -' 1) + 1 by A9, NAT_D:39 ;
((((len f) -' 1) + 1) + i1) -' j = ((((len f) -' 1) + 1) + i1) - j by A38, A37, A46, A47, NAT_D:37, XXREAL_0:2
.= ((len f) -' 1) + (1 + (i1 - j))
.= ((len f) -' 1) + (1 + (i1 -' j)) by A38, A37, A46, A47, XREAL_1:233, XXREAL_0:2 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = ((((len f) -' 1) mod ((len f) -' 1)) + (1 + (i1 -' j))) mod ((len f) -' 1) by A55, NAT_D:22
.= (0 + (1 + (i1 -' j))) mod ((len f) -' 1) by NAT_D:25
.= (i1 -' j) + 1 by A54, NAT_D:24 ;
then A56: S_Drop ((((len f) + i1) -' j),f) = (((len f) + i1) -' j) mod ((len f) -' 1) by Def1;
((((len f) - 1) + 1) + i1) - j = ((len f) - 1) + ((i1 - j) + 1) ;
then A57: ((len f) + i1) -' j = ((i1 -' j) + 1) + ((len f) -' 1) by A9, A48, A52, NAT_D:39;
((len f) -' 1) mod ((len f) -' 1) = 0 by NAT_D:25;
then S_Drop ((((len f) + i1) -' j),f) = (((i1 -' j) + 1) + 0) mod ((len f) -' 1) by A56, A57, NAT_D:22
.= ((i1 -' j) + 1) mod ((len f) -' 1) ;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 by A54, NAT_D:24; :: thesis: verum
end;
end;
end;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ; :: thesis: verum
end;
end;
end;
g . j = f . (S_Drop ((((len f) + i1) -' j),f)) by A1, A45, A46, Def3;
hence g . j = (mid (f,i1,i2)) . j by A2, A7, A6, A40, A45, A46, A43, A50, Th24; :: thesis: verum
end;
len (mid (f,i1,i2)) = len g by A2, A7, A6, A40, Th21;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) by A2, A39, A42, FINSEQ_2:9, XREAL_1:233; :: thesis: verum
end;
case n > 1 ; :: thesis: contradiction
then 1 + 1 <= n by NAT_1:13;
then A58: (((len f) + i1) -' (len g)) - i2 >= ((len f) -' 1) * (1 + 1) by A35, XREAL_1:64;
A59: (len f) - i2 <= (len f) - 1 by A7, XREAL_1:10;
(i1 + 1) + 0 < (i1 + 1) + (len g) by A3, XREAL_1:8;
then (i1 + 1) - (len g) < ((i1 + 1) + (len g)) - (len g) by XREAL_1:14;
then ((i1 - (len g)) + 1) - i2 < (i1 + 1) - i2 by XREAL_1:14;
then A60: ((len f) - 1) + (((i1 - (len g)) - i2) + 1) < ((len f) - 1) + ((i1 + 1) - i2) by XREAL_1:8;
(i1 + 1) - i2 <= (len f) - i2 by A5, XREAL_1:9;
then (i1 + 1) - i2 <= (len f) - 1 by A59, XXREAL_0:2;
then ((len f) - 1) + ((i1 + 1) - i2) <= ((len f) - 1) + ((len f) - 1) by XREAL_1:7;
then (((len f) + i1) - (len g)) - i2 < ((len f) - 1) + ((len f) - 1) by A60, XXREAL_0:2;
hence contradiction by A24, A10, A58, NAT_D:37; :: thesis: verum
end;
end;
end;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) ; :: thesis: verum
end;
case A61: (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
( ex n being Nat st
( ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) & (((len f) + i1) -' (len g)) mod ((len f) -' 1) < (len f) -' 1 ) or ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 & (len f) -' 1 = 0 ) ) by NAT_D:def 2;
then consider n being Nat such that
A62: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) by A9, NAT_D:39;
A63: ((len f) + i1) -' (len g) = i2 * n by A31, A61, A62, Def1;
now
assume n = 0 ; :: thesis: contradiction
then A64: len g >= (len f) + i1 by A61, A62, NAT_D:36;
len f <= (len f) + i1 by NAT_1:11;
hence contradiction by A24, A64, XXREAL_0:2; :: thesis: verum
end;
then A65: n >= 0 + 1 by NAT_1:13;
A66: now
per cases ( n > 1 or n = 1 ) by A65, XXREAL_0:1;
case A67: n > 1 ; :: thesis: len g = (i1 -' i2) + 1
A68: ((len f) -' 1) + ((len f) -' 1) = ((len f) -' 1) * (1 + 1) ;
(i1 + 1) + 1 <= (len f) + (len g) by A5, A3, XREAL_1:7;
then (1 + (i1 + 1)) - (len g) <= ((len f) + (len g)) - (len g) by XREAL_1:9;
then (1 + ((i1 + 1) - (len g))) - 1 <= (len f) - 1 by XREAL_1:9;
then ((len f) - 1) + ((i1 + 1) - (len g)) <= ((len f) - 1) + ((len f) - 1) by XREAL_1:6;
then ((len f) + i1) - (len g) <= ((len f) - 1) + ((len f) - 1) ;
then A69: ((len f) + i1) -' (len g) <= ((len f) -' 1) + ((len f) -' 1) by A24, A10, NAT_D:37;
A70: n >= 1 + 1 by A67, NAT_1:13;
now
per cases ( n > 1 + 1 or n = 1 + 1 ) by A70, XXREAL_0:1;
case A71: n = 1 + 1 ; :: thesis: len g = (i1 -' i2) + 1
then A72: (((len f) - 1) + (1 + i1)) - (len g) = ((len f) -' 1) + ((len f) -' 1) by A24, A61, A62, NAT_D:37;
then 1 + ((len f) -' 1) <= ((1 + i1) - ((len f) -' 1)) + ((len f) -' 1) by A3, A10, XREAL_1:6;
then 1 + ((len f) - 1) <= 1 + i1 by A9, NAT_D:39;
then A73: len f = i1 + 1 by A5, XXREAL_0:1;
then i2 = i1 by A61, A62, A63, A71, NAT_D:34;
then i1 -' i2 = 0 by XREAL_1:232;
hence len g = (i1 -' i2) + 1 by A10, A72, A73; :: thesis: verum
end;
end;
end;
hence len g = (i1 -' i2) + 1 ; :: thesis: verum
end;
case A74: n = 1 ; :: thesis: contradiction
((len f) + i1) -' (len g) = ((len f) + i1) - (len g) by A24, NAT_D:37;
then (len f) + i1 = i2 + (len g) by A63, A74;
hence contradiction by A2, A24, XREAL_1:8; :: thesis: verum
end;
end;
end;
A75: dom g = Seg (len g) by FINSEQ_1:def 3;
A76: for j being Nat st j in dom g holds
g . j = (mid (f,i1,i2)) . j
proof
let j be Nat; :: thesis: ( j in dom g implies g . j = (mid (f,i1,i2)) . j )
A77: j in NAT by ORDINAL1:def 12;
assume A78: j in dom g ; :: thesis: g . j = (mid (f,i1,i2)) . j
then A79: 1 <= j by A75, FINSEQ_1:1;
A80: j <= len g by A75, A78, FINSEQ_1:1;
1 - 1 <= i2 - 1 by A7, XREAL_1:9;
then A81: i1 - 0 >= i1 - (i2 - 1) by XREAL_1:10;
A82: (i1 -' i2) + 1 = (i1 - i2) + 1 by A2, XREAL_1:233
.= i1 - (i2 - 1) ;
then A83: (i1 -' j) + 1 = (i1 - j) + 1 by A66, A80, A81, XREAL_1:233, XXREAL_0:2;
A84: j <= i1 by A66, A80, A82, A81, XXREAL_0:2;
A85: now
per cases ( ((len f) + i1) -' j = (len f) -' 1 or ((len f) + i1) -' j <> (len f) -' 1 ) ;
case ((len f) + i1) -' j = (len f) -' 1 ; :: thesis: contradiction
then ((len f) + i1) - j = (len f) -' 1 by A66, A80, A82, A81, NAT_D:37, XXREAL_0:2
.= (len f) - 1 by A9, NAT_D:39 ;
then i1 - j = - 1 ;
hence contradiction by A84, XREAL_1:48; :: thesis: verum
end;
case ((len f) + i1) -' j <> (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
(i1 + 1) + 0 < (len f) + j by A5, A79, XREAL_1:8;
then (i1 + 1) - j < ((len f) + j) - j by XREAL_1:9;
then ((i1 + 1) - j) - 1 < (len f) - 1 by XREAL_1:9;
then i1 - j < (len f) - 1 ;
then i1 -' j < (len f) -' 1 by A10, A66, A80, A82, A81, XREAL_1:233, XXREAL_0:2;
then A86: (i1 -' j) + 1 <= (len f) -' 1 by NAT_1:13;
A87: ((len f) + i1) -' j = ((len f) + i1) - j by A66, A80, A82, A81, NAT_D:37, XXREAL_0:2;
now
per cases ( (i1 -' j) + 1 = (len f) -' 1 or (i1 -' j) + 1 < (len f) -' 1 ) by A86, XXREAL_0:1;
case A88: (i1 -' j) + 1 = (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
((len f) + i1) -' j = ((((len f) - 1) + 1) + i1) - j by A66, A80, A82, A81, NAT_D:37, XXREAL_0:2
.= ((len f) -' 1) + ((i1 - j) + 1) by A10
.= ((len f) -' 1) + ((len f) -' 1) by A66, A80, A82, A81, A88, XREAL_1:233, XXREAL_0:2 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = 0 by Th8;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 by A88, Def1; :: thesis: verum
end;
case A89: (i1 -' j) + 1 < (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
A90: len f = ((len f) - 1) + 1
.= ((len f) -' 1) + 1 by A9, NAT_D:39 ;
((((len f) -' 1) + 1) + i1) -' j = ((((len f) -' 1) + 1) + i1) - j by A66, A80, A82, A81, NAT_D:37, XXREAL_0:2
.= ((len f) -' 1) + (1 + (i1 - j))
.= ((len f) -' 1) + (1 + (i1 -' j)) by A66, A80, A82, A81, XREAL_1:233, XXREAL_0:2 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = ((((len f) -' 1) mod ((len f) -' 1)) + (1 + (i1 -' j))) mod ((len f) -' 1) by A90, NAT_D:22
.= (0 + (1 + (i1 -' j))) mod ((len f) -' 1) by NAT_D:25
.= (i1 -' j) + 1 by A89, NAT_D:24 ;
then A91: S_Drop ((((len f) + i1) -' j),f) = (((len f) + i1) -' j) mod ((len f) -' 1) by Def1;
((((len f) - 1) + 1) + i1) - j = ((len f) - 1) + ((i1 - j) + 1) ;
then A92: ((len f) + i1) -' j = ((i1 -' j) + 1) + ((len f) -' 1) by A9, A83, A87, NAT_D:39;
((len f) -' 1) mod ((len f) -' 1) = 0 by NAT_D:25;
then S_Drop ((((len f) + i1) -' j),f) = (((i1 -' j) + 1) + 0) mod ((len f) -' 1) by A91, A92, NAT_D:22
.= ((i1 -' j) + 1) mod ((len f) -' 1) ;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 by A89, NAT_D:24; :: thesis: verum
end;
end;
end;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ; :: thesis: verum
end;
end;
end;
g . j = f . (S_Drop ((((len f) + i1) -' j),f)) by A1, A79, A80, Def3;
hence g . j = (mid (f,i1,i2)) . j by A2, A7, A6, A66, A79, A80, A77, A85, Th24; :: thesis: verum
end;
len (mid (f,i1,i2)) = len g by A2, A7, A6, A66, Th21;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) by A66, A76, FINSEQ_2:9; :: thesis: verum
end;
end;
end;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) ; :: thesis: verum
end;
end;
end;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) ; :: thesis: verum