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_{1}[ 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 S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[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

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

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 S

S

proof

A21:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A2: S

thus S

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 )

A13: for i being Element of NAT st i in dom (a | n) holds

(a | n) . i = (b | n) . i

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;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

A12:
Seg n c= Seg (n + 1)
by A6, FINSEQ_1:5;
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;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

A13: for i being Element of NAT st i in dom (a | n) holds

(a | n) . i = (b | n) . i

proof

len (b | n) = n
by A4, A6, FINSEQ_1:59;
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;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

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

proof

for n being Nat holds S
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;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

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