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 & len b = n ) and
A2: for i being Element of NAT st i in Seg n holds
a . i = b . i ; :: thesis: Sum a = Sum b
A3: ( dom a = Seg n & dom b = Seg n ) by A1, FINSEQ_1:def 3;
set c = b;
reconsider c = b as FinSequence of REAL ;
A4: Sum a = Sum c by A1, A2, A3, Lm7;
( len b = len c & ( for i being Element of NAT st i in dom b holds
b . i = c . i ) ) ;
hence Sum a = Sum b by A4, Lm3; :: thesis: verum