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

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 Def11;
A5: f . 1 = (accum f) . 1 by Def11;
A7: Sum f = (accum f) . (len f) by Def10, A3;
deffunc H₁( set ) -> set = IFIN $1,((len f) + 1),(IFEQ $1,0 ,(0. (RealVectSpace (Seg n))),((accum f) /. $1)),(0. (RealVectSpace (Seg n)));
A8: 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 A9: 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 A9, 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 A9, 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
A10: for x being set st x in NAT holds
f3 . x = H₁(x) from FUNCT_2:sch 2(A8);
A11: 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
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 A3, XREAL_1:8;
then A16: j + 1 in (len f) + 1 by NAT_1:45;
A17: 0 in (len f) + 1 by NAT_1:45;
A18: f3 . j = IFIN j,((len f) + 1),(IFEQ j,0 ,(0. (RealVectSpace (Seg n))),((accum f) /. j)),(0. (RealVectSpace (Seg n))) by A10
.= IFEQ j,0 ,(0. (RealVectSpace (Seg n))),((accum f) /. j) by A15, A17, MATRIX_7:def 1
.= 0. (RealVectSpace (Seg n)) by A15, 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 A10
.= IFEQ (j + 1),0 ,(0. (RealVectSpace (Seg 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, A4, A5, A14, A15, FINSEQ_4:24
.= (f3 . j) + v by A13, A18, RLVECT_1:10 ; :: thesis: verum

end;

suppose A19: 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, A12, XXREAL_0:2;
then A20: j in (len f) + 1 by NAT_1:45;
A21: f3 . j = IFIN j,((len f) + 1),(IFEQ j,0 ,(0. (RealVectSpace (Seg n))),((accum f) /. j)),(0. (RealVectSpace (Seg n))) by A10
.= IFEQ j,0 ,(0. (RealVectSpace (Seg 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:8;
then A24: 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. (RealVectSpace (Seg n))),((accum f) /. (j + 1))),(0. (RealVectSpace (Seg n))) by A10
.= IFEQ (j + 1),0 ,(0. (RealVectSpace (Seg 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 A4, A14, A22, FINSEQ_4:24
.= ((accum f) /. j) + (f /. (j + 1)) by A1, Def11, A12, A23
.= (f3 . j) + v by A1, A13, A14, A22, A21, FINSEQ_4:24 ; :: thesis: verum

end;

end;

end;

len f < (len f) + 1 by XREAL_1:31;
then A25: len f in (len f) + 1 by NAT_1:45;
A26: 0 + 1 <= len f by A3, NAT_1:13;
A27: 0 in (len f) + 1 by NAT_1:45;
A28: f3 . 0 = IFIN 0 ,((len f) + 1),(IFEQ 0 ,0 ,(0. (RealVectSpace (Seg n))),((accum f) /. 0 )),(0. (RealVectSpace (Seg n))) by A10
.= IFEQ 0 ,0 ,(0. (RealVectSpace (Seg n))),((accum f) /. 0 ) by A27, MATRIX_7:def 1
.= 0. (RealVectSpace (Seg n)) by FUNCOP_1:def 8 ;
f3 . (len g) = H₁( len f) by A1, A10
.= IFEQ (len f),0 ,(0. (RealVectSpace (Seg n))),((accum f) /. (len f)) by A25, MATRIX_7:def 1
.= (accum f) /. (len f) by A3, FUNCOP_1:def 8
.= Sum f by A4, A7, A26, FINSEQ_4:24 ;
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 A28, A11; :: thesis: verum

end;

case A29: 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)));
A30: 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, A29;
A31: (NAT --> (0. (RealVectSpace (Seg n)))) . (len g) = 0* n by FUNCOP_1:13;
A32: (NAT --> (0. (RealVectSpace (Seg n)))) . 0 = 0. (RealVectSpace (Seg n)) by FUNCOP_1:13;
Sum f = 0* n by A29, Def10;
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 A31, A32, A30; :: thesis: verum

end;

end;

end;

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