let n1, n2 be Element of NAT ; :: thesis: ( i <= Sum (f | n1) & n1 in dom f & ( for j being Nat st i <= Sum (f | j) holds
n1 <= j ) & i <= Sum (f | n2) & n2 in dom f & ( for j being Nat st i <= Sum (f | j) holds
n2 <= j ) implies n1 = n2 )
assume that
A7: ( i <= Sum (f | n1) & n1 in dom f & ( for j being Nat st i <= Sum (f | j) holds
n1 <= j ) ) and
A8: ( i <= Sum (f | n2) & n2 in dom f & ( for j being Nat st i <= Sum (f | j) holds
n2 <= j ) ) ; :: thesis: n1 = n2
( n1 <= n2 & n2 <= n1 ) by A7, A8;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum