let X be RealNormSpace; :: thesis:
defpred S₁[ Nat] means for m being Nat
for a being Function of [:(Seg $1),(Seg m):],X
for p, q being FinSequence of X st dom p = Seg $1 & ( for i being Nat st i in dom p holds
ex r being FinSequence of X st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of X st
( dom s = Seg $1 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) holds
Sum p = Sum q;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A3: Seg n c= Seg (n + 1) by FINSEQ_1:5, NAT_1:11;

let m be Nat; :: thesis:
let a be Function of [:(Seg (n + 1)),(Seg m):],X; :: thesis:
let p, q be FinSequence of X; :: thesis:
assume that
A4: ( dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of X st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) ) ) ) and
A5: ( dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of X st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) ) ; :: thesis:
A6: len p = n + 1 by A4, FINSEQ_1:def 3;
set a0 = a | [:(Seg n),(Seg m):];
[:(Seg n),(Seg m):] c= [:(Seg (n + 1)),(Seg m):] by A3, ZFMISC_1:95;
then reconsider a0 = a | [:(Seg n),(Seg m):] as Function of [:(Seg n),(Seg m):],X by FUNCT_2:32;
A7: dom a0 = [:(Seg n),(Seg m):] by FUNCT_2:def 1;
deffunc H₁( Nat) -> set = a . [(n + 1),$1];
reconsider p0 = p | (Seg n) as FinSequence of X by FINSEQ_1:18;
A8: dom p0 = Seg n by A4, A3, RELAT_1:62;
then A9: len p0 = n by FINSEQ_1:def 3;

A10: now :: thesis:

let i be Nat; :: thesis:
assume A11: i in dom p0 ; :: thesis:
then consider r being FinSequence of X such that
A12: ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) ) by A4, A8, FINSEQ_2:8;
take r = r; :: thesis:
thus ( dom r = Seg m & p0 . i = Sum r ) by A11, A12, FUNCT_1:47; :: thesis:
thus for j being Nat st j in dom r holds
r . j = a0 . (i,j) :: thesis:

proof

let j be Nat; :: thesis:
assume A13: j in dom r ; :: thesis:
then r . j = a . (i,j) by A12;
hence r . j = a0 . (i,j) by A8, A11, A12, A13, ZFMISC_1:87, A7, FUNCT_1:47; :: thesis:

end;

reconsider m = m as Element of NAT by ORDINAL1:def 12;
consider an being FinSequence such that
A14: ( len an = m & ( for j being Nat st j in dom an holds
an . j = H₁(j) ) ) from FINSEQ_1:sch 2();
A15: dom an = Seg m by A14, FINSEQ_1:def 3;

now :: thesis:

let i be Nat; :: thesis:
assume A16: i in dom an ; :: thesis:
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then [(n + 1),i] in [:(Seg (n + 1)),(Seg m):] by A16, A15, ZFMISC_1:87;
then a . ((n + 1),i) in the carrier of X by FUNCT_2:5;
hence an . i in the carrier of X by A16, A14; :: thesis:

end;

then reconsider an = an as FinSequence of X by FINSEQ_2:12;
A17: Sum an = p . (n + 1)

proof

consider r being FinSequence of X such that
A18: ( dom r = Seg m & p . (n + 1) = Sum r & ( for j being Nat st j in dom r holds
r . j = a . ((n + 1),j) ) ) by A4, FINSEQ_1:4;

now :: thesis:

let j be Nat; :: thesis:
assume A19: j in dom r ; :: thesis:
then r . j = a . ((n + 1),j) by A18;
hence r . j = an . j by A14, A15, A18, A19; :: thesis:

end;

hence Sum an = p . (n + 1) by A14, FINSEQ_1:def 3, A18, FINSEQ_1:13; :: thesis:

end;

set q0 = q - an;
A20: dom (q - an) = (dom q) /\ (dom an) by VFUNCT_1:def 2;
then reconsider q0 = q - an as FinSequence by A15, A5, FINSEQ_1:def 2;
for i being Nat st i in dom q0 holds
q0 . i in the carrier of X

proof

let i be Nat; :: thesis:
assume i in dom q0 ; :: thesis:
then q0 . i = (q - an) /. i by PARTFUN1:def 6;
hence q0 . i in the carrier of X ; :: thesis:

end;

then reconsider q0 = q0 as FinSequence of the carrier of X by FINSEQ_2:12;
A21: len q0 = m by A5, A15, A20, FINSEQ_1:def 3;

A22: now :: thesis:

let j be Nat; :: thesis:
assume A23: j in dom q0 ; :: thesis:
consider s being FinSequence of X such that
A24: ( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) by A5, A15, A20, A23;
A25: s . (n + 1) = a . ((n + 1),j) by A24, FINSEQ_1:4;
reconsider sn = s | (Seg n) as FinSequence of X by FINSEQ_1:18;
take sn = sn; :: thesis:
A26: len s = n + 1 by A24, FINSEQ_1:def 3;
an /. j = an . j by A23, A15, A5, A20, PARTFUN1:def 6;
then an /. j = s . (n + 1) by A25, A14, A15, A5, A20, A23;
then A27: an /. j = s . (len s) by A24, FINSEQ_1:def 3;
thus A28: dom sn = Seg n by A24, A3, RELAT_1:62; :: thesis:
then A29: len s = (len sn) + 1 by A26, FINSEQ_1:def 3;
q /. j = Sum s by A24, A23, A5, A15, A20, PARTFUN1:def 6;
then (q /. j) - (an /. j) = ((Sum sn) + (an /. j)) - (an /. j) by A29, A28, RLVECT_1:38, A27
.= (Sum sn) + ((an /. j) - (an /. j)) by RLVECT_1:def 3 ;
then (q /. j) - (an /. j) = (Sum sn) + (0. X) by RLVECT_1:15;
then q0 /. j = Sum sn by A23, VFUNCT_1:def 2;
hence q0 . j = Sum sn by A23, PARTFUN1:def 6; :: thesis:
thus for i being Nat st i in dom sn holds
sn . i = a0 . (i,j) :: thesis:

proof

let i be Nat; :: thesis:
assume A30: i in dom sn ; :: thesis:
sn . i = s . i by A30, FUNCT_1:47;
then sn . i = a . (i,j) by A24, A28, A30, A3;
hence sn . i = a0 . (i,j) by A5, A15, A20, A23, A28, A30, ZFMISC_1:87, A7, FUNCT_1:47; :: thesis:

end;

for i being Nat st 1 <= i & i <= len q holds
q /. i = (q0 /. i) + (an /. i)

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i <= len q ) ; :: thesis:
then i in dom q by FINSEQ_3:25;
then (q0 /. i) + (an /. i) = ((q /. i) - (an /. i)) + (an /. i) by A5, A15, A20, VFUNCT_1:def 2
.= (q /. i) - ((an /. i) - (an /. i)) by RLVECT_1:29 ;
then (q0 /. i) + (an /. i) = (q /. i) - (0. X) by RLVECT_1:15;
hence q /. i = (q0 /. i) + (an /. i) ; :: thesis:

end;

then A31: q0 + an = q by A5, A15, A20, BINOM:def 1;
Sum p = (Sum p0) + (Sum an) by A8, A6, A9, RLVECT_1:38, A17;
then Sum p = (Sum q0) + (Sum an) by A2, A10, A8, A5, A15, A20, A22;
hence Sum p = Sum q by A31, INTEGR18:1, A14, A21; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

now :: thesis:

let m be Nat; :: thesis:
let a be Function of [:(Seg 0),(Seg m):],X; :: thesis:
let p, q be FinSequence of X; :: thesis:
assume that
A32: dom p = Seg 0 and
for i being Nat st i in dom p holds
ex r being FinSequence of X st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) ) and
dom q = Seg m and
A33: for j being Nat st j in dom q holds
ex s being FinSequence of X st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ; :: thesis:

A34: now :: thesis:

let z be object ; :: thesis:
assume A35: z in dom q ; :: thesis:
then reconsider j = z as Nat ;
consider s being FinSequence of X such that
A36: ( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) by A33, A35;
s = <*> the carrier of X by A36;
hence q . z = 0. X by A36, RLVECT_1:43; :: thesis:

end;

A37: p = <*> the carrier of X by A32;
A38: len q = len q ;

now :: thesis:

let k be Nat; :: thesis:
let v be Element of X; :: thesis:
assume A39: ( k in dom q & v = q . k ) ; :: thesis:
then q . k = 0. X by A34;
hence q . k = - v by A39; :: thesis:

end;

then Sum q = - (Sum q) by A38, RLVECT_1:40;
then Sum q = 0. X by RLVECT_1:19;
hence Sum p = Sum q by RLVECT_1:43, A37; :: thesis:

end;

then A40: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A40, A1); :: thesis: