thus for m1, m2 being Nat st ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 <= r2 ) & ( for j being 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 Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) holds
m1 = m2 :: thesis: verum

proof

let m1, m2 be Nat; :: thesis: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 <= r2 ) & ( for j being 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 Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) implies m1 = m2 )
assume A50: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds
r1 <= r2 ) & ( for j being 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 Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . m2 holds
m2 <= j ) ) ) ) ; :: thesis: m1 = m2
then ( f . m2 <= f . m1 & f . m1 <= f . m2 ) ;
then f . m1 = f . m2 by XXREAL_0:1;
then ( m1 <= m2 & m2 <= m1 ) by A50;
hence m1 = m2 by XXREAL_0:1; :: thesis: verum

end;