thus for m1, m2 being Element of NAT st ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds
m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) holds
m1 = m2 :: thesis: verum

proof

let m1, m2 be Element of NAT ; :: thesis: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds
m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) implies m1 = m2 )
assume A37: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds
m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) ) ; :: thesis: m1 = m2
then A38: f . m2 >= f . m1 ;
f . m1 >= f . m2 by A37;
then A39: f . m1 = f . m2 by A38, XXREAL_0:1;
then A40: m1 >= m2 by A37;
m2 >= m1 by A37, A39;
hence m1 = m2 by A40, XXREAL_0:1; :: thesis: verum

end;