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
per cases ( X <> {} or X = {} ) ;
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;
suppose X = {} ; :: thesis: F1 = F2
hence F1 = F2 by A7, A9; :: thesis: verum
end;
end;