let n be Element of NAT ; :: thesis: for f being FinSequence of REAL n
for g being FinSequence of the carrier of (REAL-US n) st f = g holds
Sum f = Sum g
let f be FinSequence of REAL n; :: thesis: for g being FinSequence of the carrier of (REAL-US n) st f = g holds
Sum f = Sum g
let g be FinSequence of the carrier of (REAL-US n); :: thesis: ( f = g implies Sum f = Sum g )
set V = REAL-US n;
assume A1: f = g ; :: thesis: Sum f = Sum g

now

per cases ( len f > 0 or len f <= 0 ) ;

case A2: len f > 0 ; :: thesis: ex f2 being Function of NAT ,the carrier of (REAL-US n) st
( Sum f = f2 . (len g) & f2 . 0 = 0. (REAL-US n) & ( for j being Element of NAT
for v being Element of (REAL-US n) st j < len g & v = g . (j + 1) holds
f2 . (j + 1) = (f2 . j) + v ) )

set g2 = accum f;
A3: len f = len (accum f) by Def11;
A4: f . 1 = (accum f) . 1 by Def11;
A6: Sum f = (accum f) . (len f) by A2, Def10;
deffunc H₁( set ) -> set = IFIN $1,((len f) + 1),(IFEQ $1,0 ,(0. (REAL-US n)),((accum f) /. $1)),(0. (REAL-US n));
A7: for x being set st x in NAT holds
H₁(x) in the carrier of (REAL-US n)

proof

let x be set ; :: thesis: ( x in NAT implies H₁(x) in the carrier of (REAL-US n) )
assume x in NAT ; :: thesis: H₁(x) in the carrier of (REAL-US n)
then reconsider nx = x as Element of NAT ;

per cases ( nx in (len f) + 1 or not nx in (len f) + 1 ) ;

suppose nx in (len f) + 1 ; :: thesis: H₁(x) in the carrier of (REAL-US n)

then A8: H₁(x) = IFEQ x,0 ,(0. (REAL-US n)),((accum f) /. nx) by MATRIX_7:def 1;

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: H₁(x) in the carrier of (REAL-US n)

then H₁(x) = 0. (REAL-US n) by A8, FUNCOP_1:def 8;
hence H₁(x) in the carrier of (REAL-US n) ; :: thesis: verum

end;

suppose A9: x <> 0 ; :: thesis: H₁(x) in the carrier of (REAL-US n)

A10: the carrier of (REAL-US n) = REAL n by REAL_NS1:def 6;
H₁(x) = (accum f) /. nx by A8, A9, FUNCOP_1:def 8;
hence H₁(x) in the carrier of (REAL-US n) by A10; :: thesis: verum

end;

end;

end;

suppose not nx in (len f) + 1 ; :: thesis: H₁(x) in the carrier of (REAL-US n)

then H₁(x) = 0. (REAL-US n) by MATRIX_7:def 1;
hence H₁(x) in the carrier of (REAL-US n) ; :: thesis: verum

end;

end;

end;

consider f3 being Function of NAT ,the carrier of (REAL-US n) such that
A11: for x being set st x in NAT holds
f3 . x = H₁(x) from FUNCT_2:sch 2(A7);
A12: for j being Element of NAT
for v being Element of (REAL-US n) st j < len g & v = g . (j + 1) holds
f3 . (j + 1) = (f3 . j) + v

proof

let j be Element of NAT ; :: thesis: for v being Element of (REAL-US n) st j < len g & v = g . (j + 1) holds
f3 . (j + 1) = (f3 . j) + v
let v be Element of (REAL-US n); :: thesis: ( j < len g & v = g . (j + 1) implies f3 . (j + 1) = (f3 . j) + v )
assume that
A13: j < len g and
A14: v = g . (j + 1) ; :: thesis: f3 . (j + 1) = (f3 . j) + v
A15: j + 1 <= len f by A1, A13, NAT_1:13;

per cases ( j = 0 or j <> 0 ) ;

suppose A16: j = 0 ; :: thesis: f3 . (j + 1) = (f3 . j) + v

then j + 1 < (len f) + 1 by A2, XREAL_1:8;
then A17: j + 1 in (len f) + 1 by NAT_1:45;
A18: 0 in (len f) + 1 by NAT_1:45;
A19: f3 . j = IFIN j,((len f) + 1),(IFEQ j,0 ,(0. (REAL-US n)),((accum f) /. j)),(0. (REAL-US n)) by A11
.= IFEQ j,0 ,(0. (REAL-US n)),((accum f) /. j) by A16, A18, MATRIX_7:def 1
.= 0. (REAL-US n) by A16, FUNCOP_1:def 8 ;
thus f3 . (j + 1) = IFIN (j + 1),((len f) + 1),(IFEQ (j + 1),0 ,(0. (REAL-US n)),((accum f) /. (j + 1))),(0. (REAL-US n)) by A11
.= IFEQ (j + 1),0 ,(0. (REAL-US n)),((accum f) /. (j + 1)) by A17, MATRIX_7:def 1
.= (accum f) /. 1 by A16, FUNCOP_1:def 8
.= g . (j + 1) by A1, A3, A4, A15, A16, FINSEQ_4:24
.= (f3 . j) + v by A14, A19, RLVECT_1:10 ; :: thesis: verum

end;

suppose A20: j <> 0 ; :: thesis: f3 . (j + 1) = (f3 . j) + v

len f < (len f) + 1 by XREAL_1:31;
then j < (len f) + 1 by A1, A13, XXREAL_0:2;
then A21: j in (len f) + 1 by NAT_1:45;
A22: f3 . j = IFIN j,((len f) + 1),(IFEQ j,0 ,(0. (REAL-US n)),((accum f) /. j)),(0. (REAL-US n)) by A11
.= IFEQ j,0 ,(0. (REAL-US n)),((accum f) /. j) by A21, MATRIX_7:def 1
.= (accum f) /. j by A20, FUNCOP_1:def 8 ;
A23: 0 + 1 <= j + 1 by NAT_1:13;
A24: 0 + 1 <= j by A20, NAT_1:13;
j + 1 < (len f) + 1 by A1, A13, XREAL_1:8;
then A25: j + 1 in (len f) + 1 by NAT_1:45;
thus f3 . (j + 1) = IFIN (j + 1),((len f) + 1),(IFEQ (j + 1),0 ,(0. (REAL-US n)),((accum f) /. (j + 1))),(0. (REAL-US n)) by A11
.= IFEQ (j + 1),0 ,(0. (REAL-US n)),((accum f) /. (j + 1)) by A25, MATRIX_7:def 1
.= (accum f) /. (j + 1) by FUNCOP_1:def 8
.= (accum f) . (j + 1) by A3, A15, A23, FINSEQ_4:24
.= ((accum f) /. j) + (f /. (j + 1)) by A1, Def11, A13, A24
.= (f3 . j) + v by A1, A14, A15, A23, A22, FINSEQ_4:24 ; :: thesis: verum

end;

end;

end;

len f < (len f) + 1 by XREAL_1:31;
then A26: len f in (len f) + 1 by NAT_1:45;
A27: 0 + 1 <= len f by A2, NAT_1:13;
A28: 0 in (len f) + 1 by NAT_1:45;
A29: f3 . 0 = IFIN 0 ,((len f) + 1),(IFEQ 0 ,0 ,(0. (REAL-US n)),((accum f) /. 0 )),(0. (REAL-US n)) by A11
.= IFEQ 0 ,0 ,(0. (REAL-US n)),((accum f) /. 0 ) by A28, MATRIX_7:def 1
.= 0. (REAL-US n) by FUNCOP_1:def 8 ;
f3 . (len g) = H₁( len f) by A1, A11
.= IFEQ (len f),0 ,(0. (REAL-US n)),((accum f) /. (len f)) by A26, MATRIX_7:def 1
.= (accum f) /. (len f) by A2, FUNCOP_1:def 8
.= Sum f by A3, A6, A27, FINSEQ_4:24 ;
hence ex f2 being Function of NAT ,the carrier of (REAL-US n) st
( Sum f = f2 . (len g) & f2 . 0 = 0. (REAL-US n) & ( for j being Element of NAT
for v being Element of (REAL-US n) st j < len g & v = g . (j + 1) holds
f2 . (j + 1) = (f2 . j) + v ) ) by A29, A12; :: thesis: verum

end;

case A30: len f <= 0 ; :: thesis: ex f2 being Function of NAT ,the carrier of (REAL-US n) st
( Sum f = f2 . (len g) & f2 . 0 = 0. (REAL-US n) & ( for j being Element of NAT
for v being Element of (REAL-US n) st j < len g & v = g . (j + 1) holds
f2 . (j + 1) = (f2 . j) + v ) )

set f3 = NAT --> (0. (REAL-US n));
A31: for j being Element of NAT
for v being Element of (REAL-US n) st j < len g & v = g . (j + 1) holds
(NAT --> (0. (REAL-US n))) . (j + 1) = ((NAT --> (0. (REAL-US n))) . j) + v by A1, A30;
A32: (NAT --> (0. (REAL-US n))) . (len g) = 0. (REAL-US n) by FUNCOP_1:13
.= 0* n by REAL_NS1:def 6 ;
A33: (NAT --> (0. (REAL-US n))) . 0 = 0. (REAL-US n) by FUNCOP_1:13;
Sum f = 0* n by A30, Def10;
hence ex f2 being Function of NAT ,the carrier of (REAL-US n) st
( Sum f = f2 . (len g) & f2 . 0 = 0. (REAL-US n) & ( for j being Element of NAT
for v being Element of (REAL-US n) st j < len g & v = g . (j + 1) holds
f2 . (j + 1) = (f2 . j) + v ) ) by A32, A33, A31; :: thesis: verum

end;

end;

end;

hence Sum f = Sum g by RLVECT_1:def 15; :: thesis: verum