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

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