A2:
i1 < len f
by A1, NAT_1:13;
then A3:
1 < len f
by A1, XXREAL_0:2;
then
1 + 1 <= len f
by NAT_1:13;
then A4:
(1 + 1) - 1 <= (len f) - 1
by XREAL_1:11;
then A5:
1 <= (len f) -' 1
by NAT_D:39;
A6:
i2 < len f
by A1, NAT_1:13;
A7:
i1 -' 1 = i1 - 1
by A1, XREAL_1:235;
A8:
(len f) -' 1 = (len f) - 1
by A1, A2, XREAL_1:235, XXREAL_0:2;
A9:
(i2 + 1) - 1 <= (len f) - 1
by A1, XREAL_1:11;
A10:
(i1 + 1) - 1 <= (len f) - 1
by A1, XREAL_1:11;
len f < (len f) + 1
by NAT_1:13;
then A11:
(len f) - 1 < ((len f) + 1) - 1
by XREAL_1:11;
now per cases
( i1 <= i2 or i1 > i2 )
;
case A12:
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 A13:
i1 < i2
by A1, 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 A14:
(
(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;
A15:
mid f,
i1,
i2 is_a_part>_of f,
i1,
i2
by A1, A6, A12, Th43;
A16:
len (mid f,i1,i2) = (i2 -' i1) + 1
by A1, A2, A6, A12, JORDAN3:27;
i1 + 1
<= i2
by A13, 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
(2 + i1) - i1 <= (i2 - i1) + 1
;
then
( 1
< 2 & 2
<= len (mid f,i1,i2) )
by A12, A16, XREAL_1:235;
then (mid f,i1,i2) . 2 =
f . ((2 + i1) -' 1)
by A1, A2, A6, A12, JORDAN3:27
.=
f . (((i1 + 1) + 1) - 1)
by NAT_D:37
.=
f . (i1 + 1)
;
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 A14, A15, Def4;
:: thesis: verum end; case A17:
(
(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);
A18:
(mid f,i1,1) ^ (mid f,((len f) -' 1),i2) is_a_part<_of f,
i1,
i2
by A1, A6, A13, Th46;
A19:
len (mid f,i1,1) = (i1 -' 1) + 1
by A1, A2, Th21;
now per cases
( 1 < i1 or 1 >= i1 )
;
case A20:
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 A21:
1
+ 1
<= i1
by NAT_1:13;
then A22:
f . ((i1 -' (1 + 1)) + 1) =
f . ((i1 - (1 + 1)) + 1)
by XREAL_1:235
.=
f . (i1 - 1)
.=
f . (i1 -' 1)
by A1, XREAL_1:235
;
1
+ 1
<= (i1 - 1) + 1
by A20, NAT_1:13;
then A23:
2
<= len (mid f,i1,1)
by A1, A19, XREAL_1:235;
A24:
((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . 2 =
(mid f,i1,1) . 2
by A7, A19, A21, FINSEQ_1:85
.=
f . ((i1 -' (1 + 1)) + 1)
by A2, A3, A20, A23, JORDAN3:27
;
(1 + 1) - 1
<= i1 - 1
by A21, XREAL_1:11;
then
( 1
<= i1 -' 1 &
i1 -' 1
<= (len f) -' 1 )
by A2, A7, A8, XREAL_1:11;
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 A17, A18, A22, A24, Def4, Th34;
:: thesis: verum end; case A25:
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 A26:
i1 -' 1
= 0
by XREAL_1:234;
A27:
len (mid f,i1,1) =
len (mid f,1,1)
by A1, A25, XXREAL_0:1
.=
1
by A3, Th27
;
A28:
len (mid f,((len f) -' 1),i2) =
(((len f) -' 1) -' i2) + 1
by A1, A8, A9, A11, Th21
.=
(((len f) - 1) - i2) + 1
by A8, A9, XREAL_1:235
.=
(len f) - i2
;
(len f) - i2 >= (i2 + 1) - i2
by A1, XREAL_1:11;
then A29:
1
+ 1
<= (len (mid f,i1,1)) + (len (mid f,((len f) -' 1),i2))
by A27, A28, XREAL_1:8;
A30:
1
<= (((len f) -' 1) -' i2) + 1
by NAT_1:11;
A31:
((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . 2 =
(mid f,((len f) -' 1),i2) . (2 - (len (mid f,i1,1)))
by A27, A29, JORDAN3:15
.=
(mid f,((len f) -' 1),i2) . (2 - ((i1 -' 1) + 1))
by A1, A2, Th21
.=
(mid f,((len f) -' 1),i2) . ((1 + 1) - ((1 -' 1) + 1))
by A1, A25, XXREAL_0:1
.=
(mid f,((len f) -' 1),i2) . ((1 + 1) - (0 + 1))
by XREAL_1:234
.=
f . ((((len f) -' 1) -' 1) + 1)
by A1, A8, A9, A11, A30, Th24
.=
f . ((len f) -' 1)
by A5, XREAL_1:237
;
S_Drop (i1 -' 1),
f =
S_Drop ((i1 -' 1) + ((len f) -' 1)),
f
by Th35
.=
(len f) -' 1
by A5, A26, Th34
;
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 A17, A18, A31, Def4;
:: thesis: verum 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; 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 A32:
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 A1, XXREAL_0:2;
then A33:
1
+ 1
<= i1
by NAT_1:13;
then A34:
(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 A35:
(
(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;
A36:
mid f,
i1,
i2 is_a_part<_of f,
i1,
i2
by A1, A2, A32, Th44;
A37:
len (mid f,i1,i2) = (i1 -' i2) + 1
by A1, A2, A6, A32, JORDAN3:27;
i2 + 1
<= i1
by A32, 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
(2 + i2) - i2 <= (i1 - i2) + 1
;
then
( 1
< 2 & 2
<= len (mid f,i1,i2) )
by A32, A37, XREAL_1:235;
then A38:
(mid f,i1,i2) . 2 =
f . ((i1 -' 2) + 1)
by A1, A2, A6, A32, JORDAN3:27
.=
f . ((i1 - (1 + 1)) + 1)
by A33, XREAL_1:235
.=
f . (i1 - 1)
.=
f . (i1 -' 1)
by A1, XREAL_1:235
;
i1 - 1
< (len f) - 1
by A2, XREAL_1:11;
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, A8, A34, A35, A36, A38, Def4, Th34;
:: thesis: verum end; case A39:
(
(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);
A40:
(mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) is_a_part>_of f,
i1,
i2
by A1, A2, A32, Th45;
A41:
len (mid f,i1,((len f) -' 1)) =
(((len f) -' 1) -' i1) + 1
by A1, A2, A4, A8, A10, A11, JORDAN3:27
.=
(((len f) - 1) - i1) + 1
by A8, A10, 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 A42:
(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 A41, FINSEQ_1:85
.=
f . ((2 + i1) -' 1)
by A1, A2, A4, A8, A10, A11, A41, A42, 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 A39, A40, Def4;
:: thesis: verum end; case A43:
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 A1, XXREAL_0:1;
then A44:
len (mid f,i1,((len f) -' 1)) = 1
by A4, A8, A11, Th27;
len (mid f,1,i2) =
(i2 -' 1) + 1
by A1, A3, A6, JORDAN3:27
.=
(i2 - 1) + 1
by A1, XREAL_1:235
.=
i2
;
then
1
+ 1
<= (len (mid f,i1,((len f) -' 1))) + (len (mid f,1,i2))
by A1, A44, XREAL_1:8;
then ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . 2 =
(mid f,1,i2) . (2 - ((i1 + 1) - i1))
by A44, JORDAN3:15
.=
f . 1
by A1, A3, A6, JORDAN3:27
.=
f /. 1
by A3, FINSEQ_4:24
.=
f /. (len f)
by FINSEQ_6:def 1
.=
f . (len f)
by A3, 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 A1, A39, A40, A43, Def4, XXREAL_0:1;
:: thesis: verum 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; 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;
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 b1, b2 being FinSequence of (TOP-REAL 2) st b1 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b1 . 2 = f . (S_Drop (i1 -' 1),f) ) & b2 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b2 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b2 . 2 = f . (S_Drop (i1 -' 1),f) ) holds
b1 = b2
thus
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b1 . 2 = f . (S_Drop (i1 -' 1),f) ) & b2 is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b2 . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b2 . 2 = f . (S_Drop (i1 -' 1),f) ) holds
b1 = b2
by A1, Th67; :: thesis: verum