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