let n be Element of NAT ; :: thesis: for a being FinSequence of ExtREAL
for b being FinSequence of the carrier of RLS_Real st len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds
a . i = b . i ) holds
Sum a = Sum b
let a be FinSequence of ExtREAL ; :: thesis: for b being FinSequence of the carrier of RLS_Real st len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds
a . i = b . i ) holds
Sum a = Sum b
let b be FinSequence of the carrier of RLS_Real ; :: thesis: ( len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds
a . i = b . i ) implies Sum a = Sum b )
assume that
A1: len a = n and
A2: len b = n and
A3: for i being Element of NAT st i in Seg n holds
a . i = b . i ; :: thesis: Sum a = Sum b
set c = b;
reconsider c = b as FinSequence of REAL ;
dom a = Seg n by A1, FINSEQ_1:def 3;
then A4: Sum a = Sum c by A1, A2, A3, Lm7;
A5: for i being Element of NAT st i in dom b holds
b . i = c . i ;
len b = len c ;
hence Sum a = Sum b by A4, A5, Lm3; :: thesis: verum