let a be FinSequence of ExtREAL ; :: thesis: for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b

let b be FinSequence of REAL ; :: thesis: ( len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )

defpred S1[ Nat] means for a being FinSequence of ExtREAL
for b being FinSequence of REAL st len a = \$1 & len b = \$1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let a be FinSequence of ExtREAL ; :: thesis: for b being FinSequence of REAL st len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b

let b be FinSequence of REAL ; :: thesis: ( len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )

assume that
A3: len a = n + 1 and
A4: len b = n + 1 and
A5: for i being Element of NAT st i in dom a holds
a . i = b . i ; :: thesis: Sum a = Sum b
A6: dom a = Seg (n + 1) by ;
then A7: a . (n + 1) = b . (n + 1) by ;
A8: 0 + n <= 1 + n by XREAL_1:6;
then A9: len (a | n) = n by ;
A10: Seg n c= Seg (n + 1) by ;
A11: for i being Element of NAT st i in dom (a | n) holds
(a | n) . i = (b | n) . i
proof
let i be Element of NAT ; :: thesis: ( i in dom (a | n) implies (a | n) . i = (b | n) . i )
assume i in dom (a | n) ; :: thesis: (a | n) . i = (b | n) . i
then A12: i in Seg n by ;
then A13: i <= n by FINSEQ_1:1;
then A14: (b | n) . i = b . i by FINSEQ_3:112;
(a | n) . i = a . i by ;
hence (a | n) . i = (b | n) . i by A5, A6, A10, A12, A14; :: thesis: verum
end;
len (b | n) = n by ;
then A15: Sum (a | n) = Sum (b | n) by A2, A9, A11;
b | n = b | (Seg n) by FINSEQ_1:def 15;
then A16: b = (b | n) ^ <*(b . (n + 1))*> by ;
a | n = a | (Seg n) by FINSEQ_1:def 15;
then a = (a | n) ^ <*(a . (n + 1))*> by ;
then Sum a = (Sum (a | n)) + (a . (n + 1)) by Lm4
.= (Sum (b | n)) + (b . (n + 1)) by ;
hence Sum a = Sum b by ; :: thesis: verum
end;
end;
A17: S1[ 0 ]
proof
let a be FinSequence of ExtREAL ; :: thesis: for b being FinSequence of REAL st len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b

let b be FinSequence of REAL ; :: thesis: ( len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )

assume that
A18: len a = 0 and
A19: len b = 0 and
for i being Element of NAT st i in dom a holds
a . i = b . i ; :: thesis: Sum a = Sum b
a = <*> ExtREAL by A18;
then A20: Sum a = 0. by EXTREAL1:7;
b = <*> ExtREAL by A19;
hence Sum a = Sum b by ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A17, A1);
hence ( len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b ) ; :: thesis: verum