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 S₁[ Element of 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 Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[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 A3, FINSEQ_1:def 3;
then A7: a . (n + 1) = b . (n + 1) by A5, FINSEQ_1:6;
A8: 0 + n <= 1 + n by XREAL_1:8;
then A9: len (a | n) = n by A3, FINSEQ_1:80;
A10: Seg n c= Seg (n + 1) by A8, FINSEQ_1:7;
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 A9, FINSEQ_1:def 3;
then A13: i <= n by FINSEQ_1:3;
then A14: (b | n) . i = b . i by FINSEQ_3:121;
(a | n) . i = a . i by A13, FINSEQ_3:121;
hence (a | n) . i = (b | n) . i by A5, A6, A10, A12, A14; :: thesis: verum

end;

len (b | n) = n by A4, A8, FINSEQ_1:80;
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 A4, FINSEQ_3:61;
a | n = a | (Seg n) by FINSEQ_1:def 15;
then a = (a | n) ^ <*(a . (n + 1))*> by A3, FINSEQ_3:61;
then Sum a = (Sum (a | n)) + (a . (n + 1)) by Lm4
.= (Sum (b | n)) + (b . (n + 1)) by A15, A7, SUPINF_2:1 ;
hence Sum a = Sum b by A16, RVSUM_1:104; :: thesis: verum

end;

end;

A17: S₁[ 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 X: Sum a = 0. by A18, Th4;
b = <*> ExtREAL by A19;
hence Sum a = Sum b by A19, RVSUM_1:102, X; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(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