let F1, F2 be Real_Sequence; :: thesis: ( ( for i being Element of NAT holds F1 . i = lower_sum f,(T . i) ) & ( for i being Element of NAT holds F2 . i = lower_sum f,(T . i) ) implies F1 = F2 )
assume that
A3: for i being Element of NAT holds F1 . i = lower_sum f,(T . i) and
A4: for i being Element of NAT holds F2 . i = lower_sum f,(T . 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
F1 . i = lower_sum f,(T . i) by A3
.= F2 . i by A4 ;
hence F1 . i = F2 . i ; :: thesis: verum

end;

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