let a be FinSequence of the carrier of RLS_Real; :: 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 the carrier of RLS_Real
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 the carrier of RLS_Real; :: 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: 0 + n <= 1 + n by XREAL_1:6;
then A7: len (a | n) = n by ;
A8: dom a = Seg (n + 1) by ;
A9: for i being Element of NAT st i in Seg (n + 1) holds
( a . i = a /. i & a /. i = b . i )
proof
let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies ( a . i = a /. i & a /. i = b . i ) )
assume A10: i in Seg (n + 1) ; :: thesis: ( a . i = a /. i & a /. i = b . i )
then A11: i <= n + 1 by FINSEQ_1:1;
1 <= i by ;
then a /. i = a . i by ;
hence ( a . i = a /. i & a /. i = b . i ) by A5, A8, A10; :: thesis: verum
end;
A12: Seg n c= Seg (n + 1) by ;
A13: 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 A14: i in Seg n by ;
then A15: i <= n by FINSEQ_1:1;
then A16: (b | n) . i = b . i by FINSEQ_3:112;
(a | n) . i = a . i by ;
hence (a | n) . i = (b | n) . i by A5, A8, A12, A14, A16; :: thesis: verum
end;
len (b | n) = n by ;
then A17: Sum (a | n) = Sum (b | n) by A2, A7, A13;
b | n = b | (Seg n) by FINSEQ_1:def 15;
then A18: b = (b | n) ^ <*(b . (n + 1))*> by ;
A19: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A20: a /. (n + 1) = b . (n + 1) by A9;
a | n = a | (Seg n) by FINSEQ_1:def 15;
then a = (a | n) ^ <*(a . (n + 1))*> by ;
then a = (a | n) ^ <*(a /. (n + 1))*> by ;
then Sum a = (Sum (a | n)) + (Sum <*(a /. (n + 1))*>) by RLVECT_1:41
.= (Sum (a | n)) + (a /. (n + 1)) by RLVECT_1:44
.= (Sum (b | n)) + (b . (n + 1)) by ;
hence Sum a = Sum b by ; :: thesis: verum
end;
end;
A21: S1[ 0 ]
proof
let a be FinSequence of the carrier of RLS_Real; :: 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
A22: len a = 0 and
A23: 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 = <*> the carrier of RLS_Real by A22;
then A24: Sum a = 0. RLS_Real by RLVECT_1:43;
b = <*> REAL by A23;
hence Sum a = Sum b by ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A21, 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