A45:
i1 < len f
by A1, NAT_1:13;
then A46:
1 < len f
by A1, XXREAL_0:2;
then
1 + 1 <= len f
by NAT_1:13;
then A47:
(1 + 1) - 1 <= (len f) - 1
by XREAL_1:11;
then A48:
1 <= (len f) -' 1
by NAT_D:39;
A49:
i2 < len f
by A1, NAT_1:13;
A50:
i1 -' 1 = i1 - 1
by A1, XREAL_1:235;
A51:
(len f) -' 1 = (len f) - 1
by A1, A45, XREAL_1:235, XXREAL_0:2;
A52:
(i2 + 1) - 1 <= (len f) - 1
by A1, XREAL_1:11;
A53:
(i1 + 1) - 1 <= (len f) - 1
by A1, XREAL_1:11;
len f < (len f) + 1
by NAT_1:13;
then A54:
(len f) - 1 < ((len f) + 1) - 1
by XREAL_1:11;
now per cases
( i1 <= i2 or i1 > i2 )
;
case A55:
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 A56:
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 A57:
(
(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;
A58:
mid f,
i1,
i2 is_a_part>_of f,
i1,
i2
by A1, A49, A55, Th43;
A59:
len (mid f,i1,i2) = (i2 -' i1) + 1
by A1, A45, A49, A55, JORDAN3:27;
i1 + 1
<= i2
by A56, 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 A55, A59, XREAL_1:235;
then (mid f,i1,i2) . 2 =
f . ((2 + i1) -' 1)
by A1, A45, A49, A55, 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 A57, A58, Def4;
:: thesis: verum end; case A60:
(
(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);
A61:
(mid f,i1,1) ^ (mid f,((len f) -' 1),i2) is_a_part<_of f,
i1,
i2
by A1, A49, A56, Th46;
A62:
len (mid f,i1,1) = (i1 -' 1) + 1
by A1, A45, Th21;
now per cases
( 1 < i1 or 1 >= i1 )
;
case A63:
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 A64:
1
+ 1
<= i1
by NAT_1:13;
then A65:
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 A63, NAT_1:13;
then A66:
2
<= len (mid f,i1,1)
by A1, A62, XREAL_1:235;
A67:
((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . 2 =
(mid f,i1,1) . 2
by A50, A62, A64, FINSEQ_1:85
.=
f . ((i1 -' (1 + 1)) + 1)
by A45, A46, A63, A66, JORDAN3:27
;
(1 + 1) - 1
<= i1 - 1
by A64, XREAL_1:11;
then
( 1
<= i1 -' 1 &
i1 -' 1
<= (len f) -' 1 )
by A45, A50, A51, 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 A60, A61, A65, A67, Def4, Th34;
:: thesis: verum end; case A68:
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 A69:
i1 -' 1
= 0
by XREAL_1:234;
A70:
len (mid f,i1,1) =
len (mid f,1,1)
by A1, A68, XXREAL_0:1
.=
1
by A46, Th27
;
A71:
len (mid f,((len f) -' 1),i2) =
(((len f) -' 1) -' i2) + 1
by A1, A51, A52, A54, Th21
.=
(((len f) - 1) - i2) + 1
by A51, A52, XREAL_1:235
.=
(len f) - i2
;
(len f) - i2 >= (i2 + 1) - i2
by A1, XREAL_1:11;
then A72:
1
+ 1
<= (len (mid f,i1,1)) + (len (mid f,((len f) -' 1),i2))
by A70, A71, XREAL_1:8;
A73:
(i2 + 1) - 1
<= (len f) - 1
by A1, XREAL_1:11;
A74:
1
<= (((len f) -' 1) -' i2) + 1
by NAT_1:11;
A75:
((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . 2 =
(mid f,((len f) -' 1),i2) . (2 - (len (mid f,i1,1)))
by A70, A72, JORDAN3:15
.=
(mid f,((len f) -' 1),i2) . (2 - ((i1 -' 1) + 1))
by A1, A45, Th21
.=
(mid f,((len f) -' 1),i2) . ((1 + 1) - ((1 -' 1) + 1))
by A1, A68, 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, A51, A54, A73, A74, Th24
.=
f . ((len f) -' 1)
by A48, XREAL_1:237
;
S_Drop (i1 -' 1),
f =
S_Drop ((i1 -' 1) + ((len f) -' 1)),
f
by Th35
.=
(len f) -' 1
by A48, A69, 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 A60, A61, A75, 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 A76:
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 A77:
1
+ 1
<= i1
by NAT_1:13;
then A78:
(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 A79:
(
(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;
A80:
mid f,
i1,
i2 is_a_part<_of f,
i1,
i2
by A1, A45, A76, Th44;
A81:
len (mid f,i1,i2) = (i1 -' i2) + 1
by A1, A45, A49, A76, JORDAN3:27;
i2 + 1
<= i1
by A76, 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
2
<= len (mid f,i1,i2)
by A76, A81, XREAL_1:235;
then A82:
(mid f,i1,i2) . 2 =
f . ((i1 -' 2) + 1)
by A1, A45, A49, A76, JORDAN3:27
.=
f . ((i1 - (1 + 1)) + 1)
by A77, XREAL_1:235
.=
f . (i1 - 1)
.=
f . (i1 -' 1)
by A1, XREAL_1:235
;
( 1
<= i1 -' 1 &
i1 -' 1
<= (len f) -' 1 )
by A45, A50, A51, A78, 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 A79, A80, A82, Def4, Th34;
:: thesis: verum end; case A83:
(
(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);
A84:
(mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) is_a_part>_of f,
i1,
i2
by A1, A45, A76, Th45;
A85:
len (mid f,i1,((len f) -' 1)) =
(((len f) -' 1) -' i1) + 1
by A1, A45, A47, A51, A53, A54, JORDAN3:27
.=
(((len f) - 1) - i1) + 1
by A51, A53, 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 A86:
(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 A85, FINSEQ_1:85
.=
f . ((2 + i1) -' 1)
by A1, A45, A47, A51, A53, A54, A85, A86, JORDAN3:27
.=
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 A83, A84, Def4;
:: thesis: verum end; case A87:
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 A88:
len (mid f,i1,((len f) -' 1)) = 1
by A47, A51, A54, Th27;
len (mid f,1,i2) =
(i2 -' 1) + 1
by A1, A46, A49, 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, A88, XREAL_1:8;
then ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . 2 =
(mid f,1,i2) . (2 - ((i1 + 1) - i1))
by A88, JORDAN3:15
.=
f . 1
by A1, A46, A49, JORDAN3:27
.=
f /. 1
by A46, FINSEQ_4:24
.=
f /. (len f)
by FINSEQ_6:def 1
.=
f . (len f)
by A46, 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, A83, A84, A87, 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 b1 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) ) ) & ( 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