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
A9: i <= Sum (f | n1) and
n1 in dom f and
A10: for j being Nat st i <= Sum (f | j) holds
n1 <= j and
A11: i <= Sum (f | n2) and
n2 in dom f and
A12: for j being Nat st i <= Sum (f | j) holds
n2 <= j ; :: thesis: n1 = n2
A13: n2 <= n1 by A9, A12;
n1 <= n2 by A10, A11;
hence n1 = n2 by A13, XXREAL_0:1; :: thesis: verum