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 S₁[ Element of 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 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 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 A3, FINSEQ_1:59;
A8: dom a = Seg (n + 1) by A3, FINSEQ_1:def 3;
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 A10, FINSEQ_1:1;
then a /. i = a . i by A3, A11, FINSEQ_4:15;
hence ( a . i = a /. i & a /. i = b . i ) by A5, A8, A10; :: thesis: verum

end;

A12: Seg n c= Seg (n + 1) by A6, FINSEQ_1:5;
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 A7, FINSEQ_1:def 3;
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 A15, FINSEQ_3:112;
hence (a | n) . i = (b | n) . i by A5, A8, A12, A14, A16; :: thesis: verum

end;

len (b | n) = n by A4, A6, FINSEQ_1:59;
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 A4, FINSEQ_3:55;
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 A3, FINSEQ_3:55;
then a = (a | n) ^ <*(a /. (n + 1))*> by A9, A19;
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 A17, A20, BINOP_2:def 9 ;
hence Sum a = Sum b by A18, RVSUM_1:74; :: thesis: verum

end;

end;

A21: S₁[ 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 A24, RVSUM_1:72; :: thesis: verum

end;

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