len f < (len f) + 1 by NAT_1:13;
then A49: (len f) - 1 < ((len f) + 1) - 1 by XREAL_1:9;
A50: (i2 + 1) - 1 <= (len f) - 1 by A4, XREAL_1:9;
A51: i2 < len f by A4, NAT_1:13;
A52: (i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:9;
A53: i1 -' 1 = i1 - 1 by A1, XREAL_1:233;
A54: i1 < len f by A2, NAT_1:13;
then A55: (len f) -' 1 = (len f) - 1 by A1, XREAL_1:233, XXREAL_0:2;
A56: 1 < len f by A1, A54, XXREAL_0:2;
then 1 + 1 <= len f by NAT_1:13;
then A57: (1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A58: 1 <= (len f) -' 1 by NAT_D:39;

now :: thesis: ( ( i1 <= i2 & ex g being FinSequence of (TOP-REAL 2) st
( g is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies g . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies g . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) ) or ( i1 > i2 & ex g being FinSequence of (TOP-REAL 2) st
( g is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies g . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies g . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) ) )

per cases ( i1 <= i2 or i1 > i2 ) ;

case A59: i1 <= i2 ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies g . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies g . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

then A60: i1 < i2 by A5, XXREAL_0:1;

now :: thesis: ( ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) & mid (f,i1,i2) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies (mid (f,i1,i2)) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies (mid (f,i1,i2)) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) or ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 & (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) )

per cases ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 or ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 ) ) ;

case A61: ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) ; :: thesis: ( mid (f,i1,i2) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies (mid (f,i1,i2)) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies (mid (f,i1,i2)) . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

set g = mid (f,i1,i2);
i1 + 1 <= i2 by A60, NAT_1:13;
then (1 + i1) + 1 <= i2 + 1 by XREAL_1:6;
then (2 + i1) - i1 <= (i2 + 1) - i1 by XREAL_1:9;
then A62: (2 + i1) - i1 <= (i2 - i1) + 1 ;
len (mid (f,i1,i2)) = (i2 -' i1) + 1 by A1, A3, A54, A51, A59, FINSEQ_6:118;
then 2 <= len (mid (f,i1,i2)) by A59, A62, XREAL_1:233;
then A63: (mid (f,i1,i2)) . 2 = f . ((2 + i1) -' 1) by A1, A3, A54, A51, A59, FINSEQ_6:118
.= f . (((i1 + 1) + 1) - 1) by NAT_D:37
.= f . (i1 + 1) ;
mid (f,i1,i2) is_a_part>_of f,i1,i2 by A1, A51, A59, Th31;
hence ( mid (f,i1,i2) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies (mid (f,i1,i2)) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies (mid (f,i1,i2)) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) by A61, A63; :: thesis: verum

end;

case A64: ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 ) ; :: thesis: ( (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

set g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2));
A65: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A1, A54, FINSEQ_6:187;
A66: (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2 by A1, A51, A60, Th34;

now :: thesis: ( ( 1 < i1 & (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) or ( 1 >= i1 & (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) )

per cases ( 1 < i1 or 1 >= i1 ) ;

case A67: 1 < i1 ; :: thesis: ( (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

then 1 + 1 <= (i1 - 1) + 1 by NAT_1:13;
then A68: 2 <= len (mid (f,i1,1)) by A1, A65, XREAL_1:233;
A69: i1 -' 1 <= (len f) -' 1 by A54, A53, A55, XREAL_1:9;
A70: 1 + 1 <= i1 by A67, NAT_1:13;
then A71: (1 + 1) - 1 <= i1 - 1 by XREAL_1:9;
A72: f . ((i1 -' (1 + 1)) + 1) = f . ((i1 - (1 + 1)) + 1) by A70, XREAL_1:233
.= f . (i1 - 1)
.= f . (i1 -' 1) by A1, XREAL_1:233 ;
((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = (mid (f,i1,1)) . 2 by A53, A65, A70, FINSEQ_1:64
.= f . ((i1 -' (1 + 1)) + 1) by A54, A56, A67, A68, FINSEQ_6:118 ;
hence ( (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) by A53, A64, A66, A72, A71, A69, Th22; :: thesis: verum

end;

case A73: 1 >= i1 ; :: thesis: ( (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

then i1 = 1 by A1, XXREAL_0:1;
then A74: i1 -' 1 = 0 by XREAL_1:232;
A75: S_Drop ((i1 -' 1),f) = S_Drop (((i1 -' 1) + ((len f) -' 1)),f) by Th23
.= (len f) -' 1 by A58, A74, Th22 ;
A76: 1 <= (((len f) -' 1) -' i2) + 1 by NAT_1:11;
A77: (i2 + 1) - 1 <= (len f) - 1 by A4, XREAL_1:9;
A78: (len f) - i2 >= (i2 + 1) - i2 by A4, XREAL_1:9;
1 <= len f by A56;
then S1: 1 in dom f by FINSEQ_3:25;
A79: len (mid (f,i1,1)) = len (mid (f,1,1)) by A1, A73, XXREAL_0:1
.= 1 by S1, FINSEQ_6:193 ;
len (mid (f,((len f) -' 1),i2)) = (((len f) -' 1) -' i2) + 1 by A3, A55, A50, A49, FINSEQ_6:187
.= (((len f) - 1) - i2) + 1 by A55, A50, XREAL_1:233
.= (len f) - i2 ;
then 1 + 1 <= (len (mid (f,i1,1))) + (len (mid (f,((len f) -' 1),i2))) by A79, A78, XREAL_1:6;
then ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = (mid (f,((len f) -' 1),i2)) . (2 - (len (mid (f,i1,1)))) by A79, FINSEQ_6:108
.= (mid (f,((len f) -' 1),i2)) . (2 - ((i1 -' 1) + 1)) by A1, A54, FINSEQ_6:187
.= (mid (f,((len f) -' 1),i2)) . ((1 + 1) - ((1 -' 1) + 1)) by A1, A73, XXREAL_0:1
.= (mid (f,((len f) -' 1),i2)) . ((1 + 1) - (0 + 1)) by XREAL_1:232
.= f . ((((len f) -' 1) -' 1) + 1) by A3, A55, A49, A77, A76, FINSEQ_6:190
.= f . ((len f) -' 1) by A58, XREAL_1:235 ;
hence ( (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) by A64, A66, A75; :: thesis: verum

end;

end;

end;

hence ( (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) ; :: thesis: verum

end;

end;

end;

hence ex g being FinSequence of (TOP-REAL 2) st
( g is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies g . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies g . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) ; :: thesis: verum

end;

case A80: i1 > i2 ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies g . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies g . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

then i1 > 1 by A3, XXREAL_0:2;
then A81: 1 + 1 <= i1 by NAT_1:13;
then A82: (1 + 1) - 1 <= i1 - 1 by XREAL_1:9;

now :: thesis: ( ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 & mid (f,i1,i2) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies (mid (f,i1,i2)) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies (mid (f,i1,i2)) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) or ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) & (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) )

per cases ( ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 ) or (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) ;

case A83: ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 ) ; :: thesis: ( mid (f,i1,i2) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies (mid (f,i1,i2)) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies (mid (f,i1,i2)) . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

set g = mid (f,i1,i2);
A84: i1 -' 1 <= (len f) -' 1 by A54, A53, A55, XREAL_1:9;
i2 + 1 <= i1 by A80, NAT_1:13;
then (1 + i2) + 1 <= i1 + 1 by XREAL_1:6;
then (2 + i2) - i2 <= (i1 + 1) - i2 by XREAL_1:9;
then A85: (2 + i2) - i2 <= (i1 - i2) + 1 ;
len (mid (f,i1,i2)) = (i1 -' i2) + 1 by A1, A3, A54, A51, A80, FINSEQ_6:118;
then 2 <= len (mid (f,i1,i2)) by A80, A85, XREAL_1:233;
then A86: (mid (f,i1,i2)) . 2 = f . ((i1 -' 2) + 1) by A1, A3, A54, A51, A80, FINSEQ_6:118
.= f . ((i1 - (1 + 1)) + 1) by A81, XREAL_1:233
.= f . (i1 - 1)
.= f . (i1 -' 1) by A1, XREAL_1:233 ;
mid (f,i1,i2) is_a_part<_of f,i1,i2 by A3, A54, A80, Th32;
hence ( mid (f,i1,i2) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies (mid (f,i1,i2)) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies (mid (f,i1,i2)) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) by A53, A82, A83, A86, A84, Th22; :: thesis: verum

end;

case A87: ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) ; :: thesis: ( (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

set g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2));
A88: (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2 by A3, A54, A80, Th33;
A89: len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1 by A1, A54, A57, A55, A52, A49, FINSEQ_6:118
.= (((len f) - 1) - i1) + 1 by A55, A52, XREAL_1:233
.= (len f) - i1 ;

now :: thesis: ( ( i1 + 1 < len f & (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) or ( i1 + 1 >= len f & (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) )

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

case i1 + 1 < len f ; :: thesis: ( (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

then (i1 + 1) + 1 <= len f by NAT_1:13;
then A90: (i1 + 2) - i1 <= (len f) - i1 by XREAL_1:9;
then ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = (mid (f,i1,((len f) -' 1))) . 2 by A89, FINSEQ_1:64
.= f . ((2 + i1) -' 1) by A1, A54, A57, A55, A52, A49, A89, A90, FINSEQ_6:118
.= f . (((1 + 1) + i1) - 1) by NAT_D:37
.= f . (1 + i1) ;
hence ( (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) by A87, A88; :: thesis: verum

end;

case A91: i1 + 1 >= len f ; :: thesis: ( (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) )

then S1: i1 + 1 = len f by A2, XXREAL_0:1;
then i1 <= len f by NAT_1:13;
then i1 in dom f by A1, FINSEQ_3:25;
then A92: len (mid (f,i1,((len f) -' 1))) = 1 by A55, S1, FINSEQ_6:193;
len (mid (f,1,i2)) = (i2 -' 1) + 1 by A3, A56, A51, FINSEQ_6:118
.= (i2 - 1) + 1 by A3, XREAL_1:233
.= i2 ;
then 1 + 1 <= (len (mid (f,i1,((len f) -' 1)))) + (len (mid (f,1,i2))) by A3, A92, XREAL_1:6;
then ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = (mid (f,1,i2)) . (2 - ((i1 + 1) - i1)) by A92, FINSEQ_6:108
.= f . 1 by A3, A56, A51, FINSEQ_6:118
.= f /. 1 by A56, FINSEQ_4:15
.= f /. (len f) by FINSEQ_6:def 1
.= f . (len f) by A56, FINSEQ_4:15 ;
hence ( (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) by A87, A88, A91, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ( (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) ; :: thesis: verum

end;

end;

end;

hence ex g being FinSequence of (TOP-REAL 2) st
( g is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies g . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies g . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) ; :: thesis: verum

end;

end;

end;

hence ( ex b₁ being FinSequence of (TOP-REAL 2) st
( b₁ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b₁ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b₁ . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) & ( for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b₁ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b₁ . 2 = f . (S_Drop ((i1 -' 1),f)) ) & b₂ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b₂ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b₂ . 2 = f . (S_Drop ((i1 -' 1),f)) ) holds
b₁ = b₂ ) ) by A5, Th55; :: thesis: verum