let F1, F2 be sequence of (REAL-NS n); :: thesis: ( ( for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ) implies F1 = F2 )
assume that
A2: for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) and
A3: for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ; :: thesis: F1 = F2
for i being Element of NAT holds F1 . i = F2 . i

proof

let i be Element of NAT ; :: thesis: F1 . i = F2 . i
thus F1 . i = middle_sum (f,(S . i)) by A2
.= F2 . i by A3 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:63; :: thesis: verum