per cases
( X = {} or X <> {} )
;

end;

suppose A1:
X = {}
; :: thesis: ex b_{1} being Nat st

( ( X <> {} implies ex i being Nat st

( i = b_{1} & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b_{1} = 0 ) )

( ( X <> {} implies ex i being Nat st

( i = b

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b

take
0
; :: thesis: ( ( X <> {} implies ex i being Nat st

( i = 0 & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies 0 = 0 ) )

thus ( ( X <> {} implies ex i being Nat st

( i = 0 & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies 0 = 0 ) ) by A1; :: thesis: verum

end;( i = 0 & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies 0 = 0 ) )

thus ( ( X <> {} implies ex i being Nat st

( i = 0 & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies 0 = 0 ) ) by A1; :: thesis: verum

suppose A2:
X <> {}
; :: thesis: ex b_{1} being Nat st

( ( X <> {} implies ex i being Nat st

( i = b_{1} & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b_{1} = 0 ) )

( ( X <> {} implies ex i being Nat st

( i = b

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b

then reconsider X9 = X as non empty finite Subset of NAT ;

deffunc H_{1}( Element of X9) -> Element of REAL = f /. ((2 * n) + $1);

consider x being Element of X9 such that

A3: for y being Element of X9 holds H_{1}(x) <= H_{1}(y)
from PRE_CIRC:sch 5();

reconsider x = x as Element of NAT ;

defpred S_{1}[ Nat] means ( $1 in X & f /. ((2 * n) + x) = f /. ((2 * n) + $1) );

A4: ex i being Nat st S_{1}[i]
;

consider i being Nat such that

A5: ( S_{1}[i] & ( for k being Nat st S_{1}[k] holds

i <= k ) ) from NAT_1:sch 5(A4);

take F = i; :: thesis: ( ( X <> {} implies ex i being Nat st

( i = F & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies F = 0 ) )

end;deffunc H

consider x being Element of X9 such that

A3: for y being Element of X9 holds H

reconsider x = x as Element of NAT ;

defpred S

A4: ex i being Nat st S

consider i being Nat such that

A5: ( S

i <= k ) ) from NAT_1:sch 5(A4);

take F = i; :: thesis: ( ( X <> {} implies ex i being Nat st

( i = F & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies F = 0 ) )

hereby :: thesis: ( X = {} implies F = 0 )

thus
( X = {} implies F = 0 )
by A2; :: thesis: verumassume
X <> {}
; :: thesis: ex i being Nat st

( i = F & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) )

take i = F; :: thesis: ( i = F & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) )

thus ( i = F & i in X ) by A5; :: thesis: ( ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) )

thus for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) by A3, A5; :: thesis: for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k

thus for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k by A5; :: thesis: verum

end;( i = F & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) )

take i = F; :: thesis: ( i = F & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) )

thus ( i = F & i in X ) by A5; :: thesis: ( ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) )

thus for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) by A3, A5; :: thesis: for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k

thus for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k by A5; :: thesis: verum