A6: (i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
A7: i1 -' 1 = i1 - 1 by A1, XREAL_1:235;
A8: (i2 + 1) - 1 <= (len f) - 1 by A4, XREAL_1:11;
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:11;
A11: i1 < len f by A2, NAT_1:13;
then A12: (len f) -' 1 = (len f) - 1 by A1, XREAL_1:235, 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:11;
then A15: 1 <= (len f) -' 1 by NAT_D:39;

now

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

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:8;
then (2 + i1) - i1 <= (i2 + 1) - i1 by XREAL_1:11;
then A19: (2 + i1) - i1 <= (i2 - i1) + 1 ;
len (mid f,i1,i2) = (i2 -' i1) + 1 by A1, A3, A11, A9, A16, JORDAN3:27;
then 2 <= len (mid f,i1,i2) by A16, A19, XREAL_1:235;
then A20: (mid f,i1,i2) . 2 = f . ((2 + i1) -' 1) by A1, A3, A11, A9, A16, JORDAN3:27
.= 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, Th43;
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, Def4; :: 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, Th21;
A23: (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) is_a_part<_of f,i1,i2 by A1, A9, A17, Th46;

now

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:235;
A26: i1 -' 1 <= (len f) -' 1 by A11, A7, A12, XREAL_1:11;
A27: 1 + 1 <= i1 by A24, NAT_1:13;
then A28: (1 + 1) - 1 <= i1 - 1 by XREAL_1:11;
A29: f . ((i1 -' (1 + 1)) + 1) = f . ((i1 - (1 + 1)) + 1) by A27, XREAL_1:235
.= f . (i1 - 1)
.= f . (i1 -' 1) by A1, XREAL_1:235 ;
((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . 2 = (mid f,i1,1) . 2 by A7, A22, A27, FINSEQ_1:85
.= f . ((i1 -' (1 + 1)) + 1) by A11, A13, A24, A25, JORDAN3:27 ;
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, Def4, Th34; :: 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:234;
A32: S_Drop (i1 -' 1),f = S_Drop ((i1 -' 1) + ((len f) -' 1)),f by Th35
.= (len f) -' 1 by A15, A31, Th34 ;
A33: 1 <= (((len f) -' 1) -' i2) + 1 by NAT_1:11;
A34: (len f) - i2 >= (i2 + 1) - i2 by A4, XREAL_1:11;
A35: len (mid f,i1,1) = len (mid f,1,1) by A1, A30, XXREAL_0:1
.= 1 by A13, Th27 ;
len (mid f,((len f) -' 1),i2) = (((len f) -' 1) -' i2) + 1 by A3, A12, A8, A10, Th21
.= (((len f) - 1) - i2) + 1 by A12, A8, XREAL_1:235
.= (len f) - i2 ;
then 1 + 1 <= (len (mid f,i1,1)) + (len (mid f,((len f) -' 1),i2)) by A35, A34, XREAL_1:8;
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, JORDAN3:15
.= (mid f,((len f) -' 1),i2) . (2 - ((i1 -' 1) + 1)) by A1, A11, Th21
.= (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:234
.= f . ((((len f) -' 1) -' 1) + 1) by A3, A12, A8, A10, A33, Th24
.= f . ((len f) -' 1) by A15, XREAL_1:237 ;
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, Def4; :: 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:11;

now

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:11;
i2 + 1 <= i1 by A36, NAT_1:13;
then (1 + i2) + 1 <= i1 + 1 by XREAL_1:8;
then (2 + i2) - i2 <= (i1 + 1) - i2 by XREAL_1:11;
then A41: (2 + i2) - i2 <= (i1 - i2) + 1 ;
len (mid f,i1,i2) = (i1 -' i2) + 1 by A1, A3, A11, A9, A36, JORDAN3:27;
then 2 <= len (mid f,i1,i2) by A36, A41, XREAL_1:235;
then A42: (mid f,i1,i2) . 2 = f . ((i1 -' 2) + 1) by A1, A3, A11, A9, A36, JORDAN3:27
.= f . ((i1 - (1 + 1)) + 1) by A37, XREAL_1:235
.= f . (i1 - 1)
.= f . (i1 -' 1) by A1, XREAL_1:235 ;
mid f,i1,i2 is_a_part<_of f,i1,i2 by A3, A11, A36, Th44;
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, Def4, Th34; :: 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, Th45;
A45: len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' i1) + 1 by A1, A11, A14, A12, A6, A10, JORDAN3:27
.= (((len f) - 1) - i1) + 1 by A12, A6, XREAL_1:235
.= (len f) - i1 ;

now

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:11;
then ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . 2 = (mid f,i1,((len f) -' 1)) . 2 by A45, FINSEQ_1:85
.= f . ((2 + i1) -' 1) by A1, A11, A14, A12, A6, A10, A45, A46, JORDAN3:27
.= 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, Def4; :: 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 i1 + 1 = len f by A2, XXREAL_0:1;
then A48: len (mid f,i1,((len f) -' 1)) = 1 by A14, A12, A10, Th27;
len (mid f,1,i2) = (i2 -' 1) + 1 by A3, A13, A9, JORDAN3:27
.= (i2 - 1) + 1 by A3, XREAL_1:235
.= i2 ;
then 1 + 1 <= (len (mid f,i1,((len f) -' 1))) + (len (mid f,1,i2)) by A3, A48, XREAL_1:8;
then ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . 2 = (mid f,1,i2) . (2 - ((i1 + 1) - i1)) by A48, JORDAN3:15
.= f . 1 by A3, A13, A9, JORDAN3:27
.= f /. 1 by A13, FINSEQ_4:24
.= f /. (len f) by FINSEQ_6:def 1
.= f . (len f) by A13, FINSEQ_4:24 ;
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 A2, A43, A44, A47, Def4, 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, Th67; :: thesis: verum