let m1, m2 be Nat; :: thesis: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Nat st i in dom f holds
f . i <= f . m1 ) & ( 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 st i in dom f holds
f . i <= f . m2 ) & ( 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 st i in dom f holds
f . i <= f . m1 ) & ( 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 st i in dom f holds
f . i <= f . m2 ) & ( 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