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 Def10;
A4: f . 1 = (accum f) . 1 by Def10;
A5: Sum f = (accum f) . (len f) by A2, Def11;
deffunc H₁( set ) -> set = IFIN ($1,((len f) + 1),(IFEQ ($1,0,(0. (REAL-US n)),((accum f) /. $1))),(0. (REAL-US n)));
A6: 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 A7: 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 A7, FUNCOP_1:def 8;
hence H₁(x) in the carrier of (REAL-US n) ; :: thesis: verum

end;

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

A9: the carrier of (REAL-US n) = REAL n by REAL_NS1:def 6;
H₁(x) = (accum f) /. nx by A7, A8, FUNCOP_1:def 8;
hence H₁(x) in the carrier of (REAL-US n) by A9; :: 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
A10: for x being set st x in NAT holds
f3 . x = H₁(x) from FUNCT_2:sch 2(A6);
A11: 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
A12: j < len g and
A13: v = g . (j + 1) ; :: thesis: f3 . (j + 1) = (f3 . j) + v
A14: j + 1 <= len f by A1, A12, NAT_1:13;

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

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

then j + 1 < (len f) + 1 by A2, XREAL_1:6;
then A16: j + 1 in (len f) + 1 by NAT_1:44;
A17: 0 in (len f) + 1 by NAT_1:44;
A18: f3 . j = IFIN (j,((len f) + 1),(IFEQ (j,0,(0. (REAL-US n)),((accum f) /. j))),(0. (REAL-US n))) by A10
.= IFEQ (j,0,(0. (REAL-US n)),((accum f) /. j)) by A15, A17, MATRIX_7:def 1
.= 0. (REAL-US n) by A15, 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 A10
.= IFEQ ((j + 1),0,(0. (REAL-US n)),((accum f) /. (j + 1))) by A16, MATRIX_7:def 1
.= (accum f) /. 1 by A15, FUNCOP_1:def 8
.= g . (j + 1) by A1, A3, A4, A14, A15, FINSEQ_4:15
.= (f3 . j) + v by A13, A18, RLVECT_1:4 ; :: thesis: verum

end;

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

len f < (len f) + 1 by XREAL_1:29;
then j < (len f) + 1 by A1, A12, XXREAL_0:2;
then A20: j in (len f) + 1 by NAT_1:44;
A21: f3 . j = IFIN (j,((len f) + 1),(IFEQ (j,0,(0. (REAL-US n)),((accum f) /. j))),(0. (REAL-US n))) by A10
.= IFEQ (j,0,(0. (REAL-US n)),((accum f) /. j)) by A20, MATRIX_7:def 1
.= (accum f) /. j by A19, FUNCOP_1:def 8 ;
A22: 0 + 1 <= j + 1 by NAT_1:13;
A23: 0 + 1 <= j by A19, NAT_1:13;
j + 1 < (len f) + 1 by A1, A12, XREAL_1:6;
then A24: j + 1 in (len f) + 1 by NAT_1:44;
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 A10
.= IFEQ ((j + 1),0,(0. (REAL-US n)),((accum f) /. (j + 1))) by A24, MATRIX_7:def 1
.= (accum f) /. (j + 1) by FUNCOP_1:def 8
.= (accum f) . (j + 1) by A3, A14, A22, FINSEQ_4:15
.= ((accum f) /. j) + (f /. (j + 1)) by A1, Def10, A12, A23
.= (f3 . j) + v by A1, A13, A14, A22, A21, FINSEQ_4:15 ; :: thesis: verum

end;

end;

end;

len f < (len f) + 1 by XREAL_1:29;
then A25: len f in (len f) + 1 by NAT_1:44;
A26: 0 + 1 <= len f by A2, NAT_1:13;
A27: 0 in (len f) + 1 by NAT_1:44;
A28: f3 . 0 = IFIN (0,((len f) + 1),(IFEQ (0,0,(0. (REAL-US n)),((accum f) /. 0))),(0. (REAL-US n))) by A10
.= IFEQ (0,0,(0. (REAL-US n)),((accum f) /. 0)) by A27, MATRIX_7:def 1
.= 0. (REAL-US n) by FUNCOP_1:def 8 ;
f3 . (len g) = H₁( len f) by A1, A10
.= IFEQ ((len f),0,(0. (REAL-US n)),((accum f) /. (len f))) by A25, MATRIX_7:def 1
.= (accum f) /. (len f) by A2, FUNCOP_1:def 8
.= Sum f by A3, A5, A26, FINSEQ_4:15 ;
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 A28, A11; :: thesis: verum

end;

case A29: 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));
A30: 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, A29;
A31: (NAT --> (0. (REAL-US n))) . (len g) = 0. (REAL-US n) by FUNCOP_1:7
.= 0* n by REAL_NS1:def 6 ;
A32: (NAT --> (0. (REAL-US n))) . 0 = 0. (REAL-US n) by FUNCOP_1:7;
Sum f = 0* n by A29, Def11;
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 A31, A32, A30; :: thesis: verum

end;

end;

end;

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