A6: (i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:9;
A7: i1 -' 1 = i1 - 1 by A1, XREAL_1:233;
A8: (i2 + 1) - 1 <= (len f) - 1 by A4, XREAL_1:9;
A9: i2 < len f by A4, NAT_1:13;
len f < (len f) + 1 by NAT_1:13;
then A10: (len f) - 1 < ((len f) + 1) - 1 by XREAL_1:9;
A11: i1 < len f by A2, NAT_1:13;
then A12: (len f) -' 1 = (len f) - 1 by A1, XREAL_1:233, XXREAL_0:2;
A13: 1 < len f by A1, A11, XXREAL_0:2;
then 1 + 1 <= len f by NAT_1:13;
then A14: (1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A15: 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 A16: 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 A17: 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 A18: ( (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 A17, 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 A19: (2 + i1) - i1 <= (i2 - i1) + 1 ;
len (mid (f,i1,i2)) = (i2 -' i1) + 1 by A1, A3, A11, A9, A16, FINSEQ_6:118;
then 2 <= len (mid (f,i1,i2)) by A16, A19, XREAL_1:233;
then A20: (mid (f,i1,i2)) . 2 = f . ((2 + i1) -' 1) by A1, A3, A11, A9, A16, 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, A9, A16, 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 A18, A20; :: thesis: verum

end;

case A21: ( (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));
A22: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A1, A11, FINSEQ_6:187;
A23: (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2 by A1, A9, A17, 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 A24: 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 A25: 2 <= len (mid (f,i1,1)) by A1, A22, XREAL_1:233;
A26: i1 -' 1 <= (len f) -' 1 by A11, A7, A12, XREAL_1:9;
A27: 1 + 1 <= i1 by A24, NAT_1:13;
then A28: (1 + 1) - 1 <= i1 - 1 by XREAL_1:9;
A29: f . ((i1 -' (1 + 1)) + 1) = f . ((i1 - (1 + 1)) + 1) by A27, 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 A7, A22, A27, FINSEQ_1:64
.= f . ((i1 -' (1 + 1)) + 1) by A11, A13, A24, A25, 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 A7, A21, A23, A29, A28, A26, Th22; :: thesis: verum

end;

case A30: 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 A31: i1 -' 1 = 0 by XREAL_1:232;
A32: S_Drop ((i1 -' 1),f) = S_Drop (((i1 -' 1) + ((len f) -' 1)),f) by Th23
.= (len f) -' 1 by A15, A31, Th22 ;
A33: 1 <= (((len f) -' 1) -' i2) + 1 by NAT_1:11;
A34: (len f) - i2 >= (i2 + 1) - i2 by A4, XREAL_1:9;
1 <= len f by A13;
then Z1: 1 in dom f by FINSEQ_3:25;
A35: len (mid (f,i1,1)) = len (mid (f,1,1)) by A1, A30, XXREAL_0:1
.= 1 by Z1, FINSEQ_6:193 ;
len (mid (f,((len f) -' 1),i2)) = (((len f) -' 1) -' i2) + 1 by A3, A12, A8, A10, FINSEQ_6:187
.= (((len f) - 1) - i2) + 1 by A12, A8, XREAL_1:233
.= (len f) - i2 ;
then 1 + 1 <= (len (mid (f,i1,1))) + (len (mid (f,((len f) -' 1),i2))) by A35, A34, 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 A35, FINSEQ_6:108
.= (mid (f,((len f) -' 1),i2)) . (2 - ((i1 -' 1) + 1)) by A1, A11, FINSEQ_6:187
.= (mid (f,((len f) -' 1),i2)) . ((1 + 1) - ((1 -' 1) + 1)) by A1, A30, 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, A12, A8, A10, A33, FINSEQ_6:190
.= f . ((len f) -' 1) by A15, 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 A21, A23, A32; :: 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 A36: 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 A37: 1 + 1 <= i1 by NAT_1:13;
then A38: (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 A39: ( (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);
A40: i1 - 1 < (len f) - 1 by A11, XREAL_1:9;
i2 + 1 <= i1 by A36, 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 A41: (2 + i2) - i2 <= (i1 - i2) + 1 ;
len (mid (f,i1,i2)) = (i1 -' i2) + 1 by A1, A3, A11, A9, A36, FINSEQ_6:118;
then 2 <= len (mid (f,i1,i2)) by A36, A41, XREAL_1:233;
then A42: (mid (f,i1,i2)) . 2 = f . ((i1 -' 2) + 1) by A1, A3, A11, A9, A36, FINSEQ_6:118
.= f . ((i1 - (1 + 1)) + 1) by A37, 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, A11, A36, 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 A7, A12, A38, A39, A42, A40, Th22; :: thesis: verum

end;

case A43: ( (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));
A44: (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2 by A3, A11, A36, Th33;
A45: len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1 by A1, A11, A14, A12, A6, A10, FINSEQ_6:118
.= (((len f) - 1) - i1) + 1 by A12, A6, 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 A46: (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 A45, FINSEQ_1:64
.= f . ((2 + i1) -' 1) by A1, A11, A14, A12, A6, A10, A45, A46, FINSEQ_6:118
.= f . (((1 + 1) + i1) - 1) by NAT_D:37
.= f . (i1 + 1) ;
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 A43, A44; :: thesis: verum

end;

case A47: 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 F1: 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 A48: len (mid (f,i1,((len f) -' 1))) = 1 by A12, F1, FINSEQ_6:193;
len (mid (f,1,i2)) = (i2 -' 1) + 1 by A3, A13, A9, 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, A48, XREAL_1:6;
then ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . 2 = (mid (f,1,i2)) . (2 - ((i1 + 1) - i1)) by A48, FINSEQ_6:108
.= f . 1 by A3, A13, A9, FINSEQ_6:118
.= f /. 1 by A13, FINSEQ_4:15
.= f /. (len f) by FINSEQ_6:def 1
.= f . (len f) by A13, 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 A43, A44, A47, 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 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: 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₂
thus 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