let F1, F2 be Nat; :: thesis: ( ( X <> {} implies ex i being Nat st

( i = F1 & 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 F1 = 0 ) & ( X <> {} implies ex i being Nat st

( i = F2 & 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 F2 = 0 ) implies F1 = F2 )

assume that

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

( i = F1 & 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 ) ) ) and

A7: ( X = {} implies F1 = 0 ) and

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

( i = F2 & 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 ) ) ) and

A9: ( X = {} implies F2 = 0 ) ; :: thesis: F1 = F2

( i = F1 & 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 F1 = 0 ) & ( X <> {} implies ex i being Nat st

( i = F2 & 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 F2 = 0 ) implies F1 = F2 )

assume that

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

( i = F1 & 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 ) ) ) and

A7: ( X = {} implies F1 = 0 ) and

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

( i = F2 & 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 ) ) ) and

A9: ( X = {} implies F2 = 0 ) ; :: thesis: F1 = F2

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

end;

suppose A10:
X <> {}
; :: thesis: F1 = F2

then consider j being Nat such that

A11: j = F2 and

A12: j in X and

A13: for k being Nat st k in X holds

f /. ((2 * n) + j) <= f /. ((2 * n) + k) and

A14: for k being Nat st k in X & f /. ((2 * n) + j) = f /. ((2 * n) + k) holds

j <= k by A8;

consider i being Nat such that

A15: i = F1 and

A16: i in X and

A17: for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) and

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

i <= k by A6, A10;

( f /. ((2 * n) + i) <= f /. ((2 * n) + j) & f /. ((2 * n) + j) <= f /. ((2 * n) + i) ) by A16, A17, A12, A13;

then f /. ((2 * n) + j) = f /. ((2 * n) + i) by XXREAL_0:1;

then ( i <= j & j <= i ) by A16, A18, A12, A14;

hence F1 = F2 by A15, A11, XXREAL_0:1; :: thesis: verum

end;A11: j = F2 and

A12: j in X and

A13: for k being Nat st k in X holds

f /. ((2 * n) + j) <= f /. ((2 * n) + k) and

A14: for k being Nat st k in X & f /. ((2 * n) + j) = f /. ((2 * n) + k) holds

j <= k by A8;

consider i being Nat such that

A15: i = F1 and

A16: i in X and

A17: for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) and

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

i <= k by A6, A10;

( f /. ((2 * n) + i) <= f /. ((2 * n) + j) & f /. ((2 * n) + j) <= f /. ((2 * n) + i) ) by A16, A17, A12, A13;

then f /. ((2 * n) + j) = f /. ((2 * n) + i) by XXREAL_0:1;

then ( i <= j & j <= i ) by A16, A18, A12, A14;

hence F1 = F2 by A15, A11, XXREAL_0:1; :: thesis: verum