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

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

suppose len f = 0 ; :: thesis: ex b₁ being Nat st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat st i in dom f holds
f . i <= f . b₁ ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) )

hence ex b₁ being Nat st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat st i in dom f holds
f . i <= f . b₁ ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) ) ; :: thesis: verum

end;

suppose A2: len f <> 0 ; :: thesis: ex b₁ being Nat st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat st i in dom f holds
f . i <= f . b₁ ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) )

defpred S₁[ Nat] means ex n being Nat st
( ( $1 <> 0 implies ( n <= $1 & n in dom f ) ) & ( for i being Nat st i <= $1 & i in dom f holds
f . i <= f . n ) & ( for j being Nat st j <= $1 & j in dom f & f . j = f . n holds
n <= j ) );
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[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 st i <= k & i in dom f holds
f . i <= f . n1 and
A6: for j being Nat st j <= k & j in dom f & f . j = f . n1 holds
n1 <= j ;

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

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

A8: dom f = Seg (len f) by FINSEQ_1:def 3;
A9: for i being Nat st i <= 1 & i in dom f holds
f . i <= f . 1

proof

let i be Nat; :: thesis: ( i <= 1 & i in dom f implies f . i <= f . 1 )
assume A10: i <= 1 ; :: thesis: ( not i in dom f or f . i <= f . 1 )
assume i in dom f ; :: thesis: f . i <= f . 1
then 1 <= i by FINSEQ_3:25;
hence f . i <= f . 1 by A10, 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:1;
for j being Nat st j <= 1 & j in dom f & f . j = f . 1 holds
1 <= j by A8, FINSEQ_1:1;
hence S₁[k + 1] by A7, A13, A9; :: thesis: verum

end;

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

now :: thesis: ( ( f . n1 >= f . (k + 1) & S₁[k + 1] ) or ( f . n1 < f . (k + 1) & S₁[k + 1] ) )

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 Nat st i <= k + 1 & i in dom f holds
f . i <= f . n1

proof

let i be Nat; :: thesis: ( i <= k + 1 & i in dom f implies f . i <= f . n1 )
assume that
A17: i <= k + 1 and
A18: i in dom f ; :: thesis: f . i <= f . n1

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

suppose i < k + 1 ; :: thesis: f . i <= f . n1

then i <= k by NAT_1:13;
hence f . i <= f . n1 by A5, A18; :: thesis: verum

end;

suppose i >= k + 1 ; :: thesis: f . i <= f . n1

hence f . i <= f . n1 by A15, A17, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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

proof

let j be 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

now :: thesis: ( ( j < k + 1 & n1 <= j ) or ( j >= k + 1 & n1 <= j ) )

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

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

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

end;

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

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

end;

end;

end;

hence n1 <= j ; :: thesis: verum

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 :: thesis: ( ( k + 1 > len f & S₁[k + 1] ) or ( k + 1 <= len f & S₁[k + 1] ) )

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 Nat st j <= k + 1 & j in dom f & f . j = f . n1 holds
n1 <= j

proof

let j be 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 Nat st i <= k + 1 & i in dom f holds
f . i <= f . n1

proof

let i be Nat; :: thesis: ( i <= k + 1 & i in dom f implies f . i <= f . n1 )
assume that
i <= k + 1 and
A30: i in dom f ; :: thesis: f . i <= f . n1
i <= len f by A1, A30, FINSEQ_1:1;
then i <= k by A28, XXREAL_0:2;
hence f . i <= f . n1 by A5, A30; :: thesis: verum

end;

n1 <= len f by A1, A4, A14, FINSEQ_1:1;
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 Nat st i <= k + 1 & i in dom f holds
f . i <= f . (k + 1)

proof

let i be Nat; :: thesis: ( i <= k + 1 & i in dom f implies f . i <= f . (k + 1) )
assume that
A34: i <= k + 1 and
A35: i in dom f ; :: thesis: f . i <= f . (k + 1)
set r1 = f . i;

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

suppose A38: i < k + 1 ; :: thesis: f . i <= f . (k + 1)

reconsider r3 = f . n1 as Real ;
i <= k by A38, NAT_1:13;
then f . i <= r3 by A5, A35;
hence f . i <= f . (k + 1) by A24, XXREAL_0:2; :: thesis: verum

end;

suppose i >= k + 1 ; :: thesis: f . i <= f . (k + 1)

hence f . i <= f . (k + 1) by A34, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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

proof

let j be 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:1;
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;

( ( for i being Nat st i <= 0 & i in dom f holds
f . i <= f . 1 ) & ( 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: S₁[ 0 ] ;
for k being Nat holds S₁[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 st i <= len f & i in dom f holds
f . i <= f . n1 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

proof

let j be 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:25;
hence n1 <= j by A44, A46, A47; :: thesis: verum

end;

for i being Nat st i in dom f holds
f . i <= f . n1

proof

let i be Nat; :: thesis: ( i in dom f implies f . i <= f . n1 )
assume A48: i in dom f ; :: thesis: f . i <= f . n1
then i <= len f by FINSEQ_3:25;
hence f . i <= f . n1 by A43, A48; :: thesis: verum

end;

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

end;

end;