A1: dom f = Seg (len f) by FINSEQ_1:def 3;

now

per cases ( len f = 0 or len f <> 0 ) ;

case len f = 0 ; :: thesis: ex b₁ being Element of NAT st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) )

hence ex b₁ being Element of NAT st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) ) ; :: thesis: verum

end;

case A2: len f <> 0 ; :: thesis: ex b₁ being Element of NAT st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) )

defpred S₁[ Element of NAT ] means ex n being Element of NAT st
( ( $1 <> 0 implies ( n <= $1 & n in dom f ) ) & ( for i being Element of 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 Element of NAT st j <= $1 & j in dom f & f . j = f . n holds
n <= j ) );
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider n1 being Element of NAT such that
A4: ( k <> 0 implies ( n1 <= k & n1 in dom f ) ) and
A5: for i being Element of 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 Element of NAT st j <= k & j in dom f & f . j = f . n1 holds
n1 <= j ;

now

per cases ( k = 0 or k <> 0 ) ;

case A7: k = 0 ; :: thesis: S₁[k + 1]

A8: dom f = Seg (len f) by FINSEQ_1:def 3;
A9: for i being Element of NAT
for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds
r1 >= r2

proof

let i be Element of NAT ; :: thesis: for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds
r1 >= r2
let r1, r2 be Real; :: thesis: ( i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 implies r1 >= r2 )
assume that
A10: i <= 1 and
A11: i in dom f and
A12: ( r1 = f . i & r2 = f . 1 ) ; :: thesis: r1 >= r2
1 <= i by A11, FINSEQ_3:27;
hence r1 >= r2 by A10, A12, XXREAL_0:1; :: thesis: verum

end;

len f >= 0 + 1 by A2, NAT_1:13;
then A13: 1 in dom f by A8, FINSEQ_1:3;
for j being Element of NAT st j <= 1 & j in dom f & f . j = f . 1 holds
1 <= j by A8, FINSEQ_1:3;
hence S₁[k + 1] by A7, A13, A9; :: thesis: verum

end;

case A14: k <> 0 ; :: thesis: S₁[k + 1]

now

per cases ( f . n1 <= f . (k + 1) or f . n1 > f . (k + 1) ) ;

case A15: f . n1 <= f . (k + 1) ; :: thesis: S₁[k + 1]

A16: for i being Element of NAT
for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2

proof

let i be Element of NAT ; :: thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2
let r1, r2 be Real; :: thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 )
assume that
A17: i <= k + 1 and
A18: i in dom f and
A19: ( r1 = f . i & r2 = f . n1 ) ; :: thesis: r1 >= r2

per cases ( i < k + 1 or i >= k + 1 ) ;

suppose i < k + 1 ; :: thesis: r1 >= r2

then i <= k by NAT_1:13;
hence r1 >= r2 by A5, A18, A19; :: thesis: verum

end;

suppose i >= k + 1 ; :: thesis: r1 >= r2

hence r1 >= r2 by A15, A17, A19, XXREAL_0:1; :: thesis: verum

end;

end;

end;

A20: n1 <= k + 1 by A4, A14, NAT_1:13;
A21: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds
n1 <= j

proof

let j be Element of NAT ; :: thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j )
assume that
A22: j <= k + 1 and
A23: ( j in dom f & f . j = f . n1 ) ; :: thesis: n1 <= j

per cases ( j < k + 1 or j >= k + 1 ) ;

suppose j < k + 1 ; :: thesis: n1 <= j

then j <= k by NAT_1:13;
hence n1 <= j by A6, A23; :: thesis: verum

end;

suppose j >= k + 1 ; :: thesis: n1 <= j

hence n1 <= j by A20, A22, XXREAL_0:1; :: thesis: verum

end;

end;

end;

( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A4, A14, NAT_1:13;
hence S₁[k + 1] by A16, A21; :: thesis: verum

end;

case A24: f . n1 > f . (k + 1) ; :: thesis: S₁[k + 1]

now

per cases ( k + 1 > len f or k + 1 <= len f ) ;

case A25: k + 1 > len f ; :: thesis: S₁[k + 1]

A26: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds
n1 <= j

proof

let j be Element of NAT ; :: thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j )
assume that
j <= k + 1 and
A27: ( j in dom f & f . j = f . n1 ) ; :: thesis: n1 <= j

per cases ( j < k + 1 or j >= k + 1 ) ;

suppose j < k + 1 ; :: thesis: n1 <= j

then j <= k by NAT_1:13;
hence n1 <= j by A6, A27; :: thesis: verum

end;

suppose j >= k + 1 ; :: thesis: n1 <= j

then k < j by NAT_1:13;
hence n1 <= j by A4, A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A28: k >= len f by A25, NAT_1:13;
A29: for i being Element of NAT
for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2

proof

let i be Element of NAT ; :: thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2
let r1, r2 be Real; :: thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 )
assume that
i <= k + 1 and
A30: i in dom f and
A31: ( r1 = f . i & r2 = f . n1 ) ; :: thesis: r1 >= r2
i <= len f by A1, A30, FINSEQ_1:3;
then i <= k by A28, XXREAL_0:2;
hence r1 >= r2 by A5, A30, A31; :: thesis: verum

end;

n1 <= len f by A1, A4, A14, FINSEQ_1:3;
then ( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A4, A14, A25, XXREAL_0:2;
hence S₁[k + 1] by A29, A26; :: thesis: verum

end;

case A32: k + 1 <= len f ; :: thesis: S₁[k + 1]

set n2 = k + 1;
A33: for i being Element of NAT
for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds
r1 >= r2

proof

let i be Element of NAT ; :: thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds
r1 >= r2
let r1, r2 be Real; :: thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) implies r1 >= r2 )
assume that
A34: i <= k + 1 and
A35: i in dom f and
A36: r1 = f . i and
A37: r2 = f . (k + 1) ; :: thesis: r1 >= r2

per cases ( i < k + 1 or i >= k + 1 ) ;

suppose A38: i < k + 1 ; :: thesis: r1 >= r2

reconsider r3 = f . n1 as Real ;
i <= k by A38, NAT_1:13;
then r1 >= r3 by A5, A35, A36;
hence r1 >= r2 by A24, A37, XXREAL_0:2; :: thesis: verum

end;

suppose i >= k + 1 ; :: thesis: r1 >= r2

hence r1 >= r2 by A34, A36, A37, XXREAL_0:1; :: thesis: verum

end;

end;

end;

A39: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . (k + 1) holds
k + 1 <= j

proof

let j be Element of NAT ; :: thesis: ( j <= k + 1 & j in dom f & f . j = f . (k + 1) implies k + 1 <= j )
assume that
j <= k + 1 and
A40: ( j in dom f & f . j = f . (k + 1) ) ; :: thesis: k + 1 <= j

per cases ( j < k + 1 or j >= k + 1 ) ;

suppose j < k + 1 ; :: thesis: k + 1 <= j

then j <= k by NAT_1:13;
hence k + 1 <= j by A5, A24, A40; :: thesis: verum

end;

suppose j >= k + 1 ; :: thesis: k + 1 <= j

hence k + 1 <= j ; :: thesis: verum

end;

end;

end;

1 <= 1 + k by NAT_1:12;
then ( k + 1 <> 0 implies ( k + 1 <= k + 1 & k + 1 in dom f ) ) by A1, A32, FINSEQ_1:3;
hence S₁[k + 1] by A33, A39; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

( ( for i being Element of 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 Element of NAT st j <= 0 & j in dom f & f . j = f . 1 holds
1 <= j ) ) by A1, FINSEQ_1:3, FINSEQ_3:27;
then A41: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A41, A3);
then consider n1 being Element of NAT such that
A42: ( len f <> 0 implies ( n1 <= len f & n1 in dom f ) ) and
A43: for i being Element of 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 Element of NAT st j <= len f & j in dom f & f . j = f . n1 holds
n1 <= j ;
A45: for j being Element of NAT st j in dom f & f . j = f . n1 holds
n1 <= j

proof

let j be Element of NAT ; :: thesis: ( j in dom f & f . j = f . n1 implies n1 <= j )
assume that
A46: j in dom f and
A47: f . j = f . n1 ; :: thesis: n1 <= j
j <= len f by A46, FINSEQ_3:27;
hence n1 <= j by A44, A46, A47; :: thesis: verum

end;

for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2

proof

let i be Element of NAT ; :: thesis: for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds
r1 >= r2
let r1, r2 be Real; :: thesis: ( i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 )
assume that
A48: i in dom f and
A49: ( r1 = f . i & r2 = f . n1 ) ; :: thesis: r1 >= r2
i <= len f by A48, FINSEQ_3:27;
hence r1 >= r2 by A43, A48, A49; :: thesis: verum

end;

hence ex b₁ being Element of NAT st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) ) by A2, A42, A45; :: thesis: verum

end;

end;

end;

hence ex b₁ being Element of NAT st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) ) ; :: thesis: verum