A1:
dom f = Seg (len f)
by FINSEQ_1:def 3;
now ( ( len f = 0 & ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) ) ) or ( len f <> 0 & ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) ) ) )per cases
( len f = 0 or len f <> 0 )
;
case A2:
len f <> 0
;
ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )defpred S1[
Nat]
means ex
n being
Nat st
( ( $1
<> 0 implies (
n <= $1 &
n in dom f ) ) & ( for
i being
Nat for
r1,
r2 being
Real st
i <= $1 &
i in dom f &
r1 = f . i &
r2 = f . n holds
r1 >= r2 ) & ( for
j being
Nat st
j <= $1 &
j in dom f &
f . j = f . n holds
n <= j ) );
A3:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume
S1[
k]
;
S1[k + 1]
then consider n1 being
Nat such that A4:
(
k <> 0 implies (
n1 <= k &
n1 in dom f ) )
and A5:
for
i being
Nat for
r1,
r2 being
Real st
i <= k &
i in dom f &
r1 = f . i &
r2 = f . n1 holds
r1 >= r2
and A6:
for
j being
Nat st
j <= k &
j in dom f &
f . j = f . n1 holds
n1 <= j
;
now ( ( k = 0 & S1[k + 1] ) or ( k <> 0 & S1[k + 1] ) )end;
hence
S1[
k + 1]
;
verum
end;
( ( for
i being
Nat for
r1,
r2 being
Real st
i <= 0 &
i in dom f &
r1 = f . i &
r2 = f . 1 holds
r1 >= r2 ) & ( for
j being
Nat st
j <= 0 &
j in dom f &
f . j = f . 1 holds
1
<= j ) )
by A1, FINSEQ_1:1;
then A41:
S1[
0 ]
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A41, A3);
then consider n1 being
Nat such that A42:
(
len f <> 0 implies (
n1 <= len f &
n1 in dom f ) )
and A43:
for
i being
Nat for
r1,
r2 being
Real st
i <= len f &
i in dom f &
r1 = f . i &
r2 = f . n1 holds
r1 >= r2
and A44:
for
j being
Nat st
j <= len f &
j in dom f &
f . j = f . n1 holds
n1 <= j
;
A45:
for
j being
Nat st
j in dom f &
f . j = f . n1 holds
n1 <= j
for
i being
Nat for
r1,
r2 being
Real st
i in dom f &
r1 = f . i &
r2 = f . n1 holds
r1 >= r2
hence
ex
b1 being
Nat st
( (
len f = 0 implies
b1 = 0 ) & (
len f > 0 implies (
b1 in dom f & ( for
i being
Nat for
r1,
r2 being
Real st
i in dom f &
r1 = f . i &
r2 = f . b1 holds
r1 >= r2 ) & ( for
j being
Nat st
j in dom f &
f . j = f . b1 holds
b1 <= j ) ) ) )
by A2, A42, A45;
verum end; end; end;
hence
ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
; verum