let n be Nat; :: thesis: for f being FinSequence of REAL n
for g being FinSequence of the carrier of (RealVectSpace (Seg 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 (RealVectSpace (Seg n)) st f = g holds
Sum f = Sum g
let g be FinSequence of the carrier of (RealVectSpace (Seg n)); :: thesis: ( f = g implies Sum f = Sum g )
assume A1: f = g ; :: thesis: Sum f = Sum g
set V = RealVectSpace (Seg n);
A2: REAL n = the carrier of (RealVectSpace (Seg n)) by FINSEQ_2:93;

now

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

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

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

proof

let x be set ; :: thesis: ( x in NAT implies H₁(x) in the carrier of (RealVectSpace (Seg n)) )
assume x in NAT ; :: thesis: H₁(x) in the carrier of (RealVectSpace (Seg 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 (RealVectSpace (Seg n))

then A8: H₁(x) = IFEQ (x,0,(0. (RealVectSpace (Seg 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 (RealVectSpace (Seg n))

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

end;

suppose x <> 0 ; :: thesis: H₁(x) in the carrier of (RealVectSpace (Seg n))

then H₁(x) = (accum f) /. nx by A8, FUNCOP_1:def 8;
hence H₁(x) in the carrier of (RealVectSpace (Seg n)) by A2; :: thesis: verum

end;

end;

end;

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

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

end;

end;

end;

consider f3 being Function of NAT, the carrier of (RealVectSpace (Seg n)) such that
A9: for x being set st x in NAT holds
f3 . x = H₁(x) from FUNCT_2:sch 2(A7);
A10: for j being Element of NAT
for v being Element of (RealVectSpace (Seg 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 (RealVectSpace (Seg n)) st j < len g & v = g . (j + 1) holds
f3 . (j + 1) = (f3 . j) + v
let v be Element of (RealVectSpace (Seg n)); :: thesis: ( j < len g & v = g . (j + 1) implies f3 . (j + 1) = (f3 . j) + v )
assume that
A11: j < len g and
A12: v = g . (j + 1) ; :: thesis: f3 . (j + 1) = (f3 . j) + v
A13: j + 1 <= len f by A1, A11, NAT_1:13;

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

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

then j + 1 < (len f) + 1 by A3, XREAL_1:6;
then A15: j + 1 in (len f) + 1 by NAT_1:44;
A16: 0 in (len f) + 1 by NAT_1:44;
A17: f3 . j = IFIN (j,((len f) + 1),(IFEQ (j,0,(0. (RealVectSpace (Seg n))),((accum f) /. j))),(0. (RealVectSpace (Seg n)))) by A9
.= IFEQ (j,0,(0. (RealVectSpace (Seg n))),((accum f) /. j)) by A14, A16, MATRIX_7:def 1
.= 0. (RealVectSpace (Seg n)) by A14, FUNCOP_1:def 8 ;
thus f3 . (j + 1) = IFIN ((j + 1),((len f) + 1),(IFEQ ((j + 1),0,(0. (RealVectSpace (Seg n))),((accum f) /. (j + 1)))),(0. (RealVectSpace (Seg n)))) by A9
.= IFEQ ((j + 1),0,(0. (RealVectSpace (Seg n))),((accum f) /. (j + 1))) by A15, MATRIX_7:def 1
.= (accum f) /. 1 by A14, FUNCOP_1:def 8
.= g . (j + 1) by A1, A4, A5, A13, A14, FINSEQ_4:15
.= (f3 . j) + v by A12, A17, RLVECT_1:4 ; :: thesis: verum

end;

suppose A18: 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, A11, XXREAL_0:2;
then A19: j in (len f) + 1 by NAT_1:44;
A20: f3 . j = IFIN (j,((len f) + 1),(IFEQ (j,0,(0. (RealVectSpace (Seg n))),((accum f) /. j))),(0. (RealVectSpace (Seg n)))) by A9
.= IFEQ (j,0,(0. (RealVectSpace (Seg n))),((accum f) /. j)) by A19, MATRIX_7:def 1
.= (accum f) /. j by A18, FUNCOP_1:def 8 ;
A21: 0 + 1 <= j + 1 by NAT_1:13;
A22: 0 + 1 <= j by A18, NAT_1:13;
j + 1 < (len f) + 1 by A1, A11, XREAL_1:6;
then A23: 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. (RealVectSpace (Seg n))),((accum f) /. (j + 1)))),(0. (RealVectSpace (Seg n)))) by A9
.= IFEQ ((j + 1),0,(0. (RealVectSpace (Seg n))),((accum f) /. (j + 1))) by A23, MATRIX_7:def 1
.= (accum f) /. (j + 1) by FUNCOP_1:def 8
.= (accum f) . (j + 1) by A4, A13, A21, FINSEQ_4:15
.= ((accum f) /. j) + (f /. (j + 1)) by A1, Def10, A11, A22
.= (f3 . j) + v by A1, A12, A13, A21, A20, FINSEQ_4:15 ; :: thesis: verum

end;

end;

end;

len f < (len f) + 1 by XREAL_1:29;
then A24: len f in (len f) + 1 by NAT_1:44;
A25: 0 + 1 <= len f by A3, NAT_1:13;
A26: 0 in (len f) + 1 by NAT_1:44;
A27: f3 . 0 = IFIN (0,((len f) + 1),(IFEQ (0,0,(0. (RealVectSpace (Seg n))),((accum f) /. 0))),(0. (RealVectSpace (Seg n)))) by A9
.= IFEQ (0,0,(0. (RealVectSpace (Seg n))),((accum f) /. 0)) by A26, MATRIX_7:def 1
.= 0. (RealVectSpace (Seg n)) by FUNCOP_1:def 8 ;
f3 . (len g) = H₁( len f) by A1, A9
.= IFEQ ((len f),0,(0. (RealVectSpace (Seg n))),((accum f) /. (len f))) by A24, MATRIX_7:def 1
.= (accum f) /. (len f) by A3, FUNCOP_1:def 8
.= Sum f by A4, A6, A25, FINSEQ_4:15 ;
hence ex f2 being Function of NAT, the carrier of (RealVectSpace (Seg n)) st
( Sum f = f2 . (len g) & f2 . 0 = 0. (RealVectSpace (Seg n)) & ( for j being Element of NAT
for v being Element of (RealVectSpace (Seg n)) st j < len g & v = g . (j + 1) holds
f2 . (j + 1) = (f2 . j) + v ) ) by A27, A10; :: thesis: verum

end;

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

set f3 = NAT --> (0. (RealVectSpace (Seg n)));
A29: for j being Element of NAT
for v being Element of (RealVectSpace (Seg n)) st j < len g & v = g . (j + 1) holds
(NAT --> (0. (RealVectSpace (Seg n)))) . (j + 1) = ((NAT --> (0. (RealVectSpace (Seg n)))) . j) + v by A1, A28;
A30: (NAT --> (0. (RealVectSpace (Seg n)))) . (len g) = 0* n by FUNCOP_1:7;
A31: (NAT --> (0. (RealVectSpace (Seg n)))) . 0 = 0. (RealVectSpace (Seg n)) by FUNCOP_1:7;
Sum f = 0* n by A28, Def11;
hence ex f2 being Function of NAT, the carrier of (RealVectSpace (Seg n)) st
( Sum f = f2 . (len g) & f2 . 0 = 0. (RealVectSpace (Seg n)) & ( for j being Element of NAT
for v being Element of (RealVectSpace (Seg n)) st j < len g & v = g . (j + 1) holds
f2 . (j + 1) = (f2 . j) + v ) ) by A30, A31, A29; :: thesis: verum

end;

end;

end;

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