let F1, F2 be Element of NAT ; :: thesis:
assume that
A6: ( ( X <> {} implies ex i being Element of NAT st
( i = F1 & i in X & ( for k being Element of NAT st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Element of NAT st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies F1 = 0 ) ) and
A7: ( ( X <> {} implies ex i being Element of NAT st
( i = F2 & i in X & ( for k being Element of NAT st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Element of NAT st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies F2 = 0 ) ) ; :: thesis:

per cases ;

suppose A8: X <> {} ; :: thesis:

then consider i being Element of NAT such that
A9: ( i = F1 & i in X & ( for k being Element of NAT st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Element of NAT st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) by A6;
consider j being Element of NAT such that
A10: ( j = F2 & j in X & ( for k being Element of NAT st k in X holds
f /. ((2 * n) + j) <= f /. ((2 * n) + k) ) & ( for k being Element of NAT st k in X & f /. ((2 * n) + j) = f /. ((2 * n) + k) holds
j <= k ) ) by A7, A8;
A11: f /. ((2 * n) + i) <= f /. ((2 * n) + j) by A9, A10;
f /. ((2 * n) + j) <= f /. ((2 * n) + i) by A9, A10;
then A12: f /. ((2 * n) + j) = f /. ((2 * n) + i) by A11, XXREAL_0:1;
then A13: i <= j by A9, A10;
j <= i by A9, A10, A12;
hence F1 = F2 by A9, A10, A13, XXREAL_0:1; :: thesis:

end;

suppose X = {} ; :: thesis:

hence F1 = F2 by A6, A7; :: thesis:

end;