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 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 by A1, FINSEQ_1:3;
for j being Element of NAT st j <= 0 & j in dom f & f . j = f . 1 holds
1 <= j by FINSEQ_3:27;
then A4: S₁[ 0 ] by A3;
A5: 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
A6: ( ( k <> 0 implies ( n1 <= k & n1 in dom f ) ) & ( 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 ) & ( 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;
len f > 0 by A2;
then len f >= 0 + 1 by NAT_1:13;
then A9: ( 1 <= 1 & 1 in dom f ) by A8, FINSEQ_1:3;
A10: 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 A11: ( i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 ) ; :: thesis: r1 >= r2
then ( 1 <= i & i <= len f ) by FINSEQ_3:27;
hence r1 >= r2 by A11, XXREAL_0:1; :: thesis: verum

end;

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, A9, A10; :: thesis: verum

end;

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

now

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

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

A14: n1 <= k + 1 by A6, A12, NAT_1:13;
A15: ( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A6, A12, NAT_1:13;
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 A17: ( i <= k + 1 & i in dom f & 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 A6, A17; :: thesis: verum

end;

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

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

end;

end;

end;

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 A18: ( j <= k + 1 & 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, A18; :: thesis: verum

end;

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

hence n1 <= j by A14, A18, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] by A15, A16; :: thesis: verum

end;

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

now

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

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

then A21: k >= len f by NAT_1:13;
( 1 <= n1 & n1 <= len f ) by A1, A6, A12, FINSEQ_1:3;
then A22: ( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A6, A20, XXREAL_0:2;
A23: 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 A24: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 ) ; :: thesis: r1 >= r2
then ( 1 <= i & i <= len f ) by A1, FINSEQ_1:3;
then i <= k by A21, XXREAL_0:2;
hence r1 >= r2 by A6, A24; :: thesis: verum

end;

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 A25: ( j <= k + 1 & 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, A25; :: thesis: verum

end;

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

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

end;

end;

end;

hence S₁[k + 1] by A22, A23; :: thesis: verum

end;

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

A27: 1 <= 1 + k by NAT_1:12;
set n2 = k + 1;
A28: ( k + 1 <> 0 implies ( k + 1 <= k + 1 & k + 1 in dom f ) ) by A1, A26, A27, FINSEQ_1:3;
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 . (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 A30: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) ) ; :: thesis: r1 >= r2

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

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

then A31: i <= k by NAT_1:13;
reconsider r3 = f . n1 as Real ;
r1 >= r3 by A6, A30, A31;
hence r1 >= r2 by A19, A30, XXREAL_0:2; :: thesis: verum

end;

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

hence r1 >= r2 by A30, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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 A32: ( j <= k + 1 & 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 A6, A19, A32; :: thesis: verum

end;

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

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

end;

end;

end;

hence S₁[k + 1] by A28, A29; :: 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 k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
then consider n1 being Element of NAT such that
A33: ( ( len f <> 0 implies ( n1 <= len f & n1 in dom f ) ) & ( 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 ) & ( for j being Element of NAT st j <= len f & j in dom f & f . j = f . n1 holds
n1 <= j ) ) ;
A34: 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 A35: ( i in dom f & r1 = f . i & r2 = f . n1 ) ; :: thesis: r1 >= r2
then ( 1 <= i & i <= len f ) by FINSEQ_3:27;
hence r1 >= r2 by A33, A35; :: thesis: verum

end;

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 A36: ( j in dom f & f . j = f . n1 ) ; :: thesis: n1 <= j
then ( 1 <= j & j <= len f ) by FINSEQ_3:27;
hence n1 <= j by A33, A36; :: 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, A33, A34; :: 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