let X be RealNormSpace; for n, m being Nat
for a being Function of [:(Seg n),(Seg m):],X
for p, q being FinSequence of X st dom p = Seg n & ( 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 n & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) holds
Sum p = Sum q
defpred S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
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;
now for m being Nat
for a being Function of [:(Seg (n + 1)),(Seg m):],X
for p, q being FinSequence of X st 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) ) ) ) & 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) ) ) ) holds
Sum p = Sum qlet m be
Nat;
for a being Function of [:(Seg (n + 1)),(Seg m):],X
for p, q being FinSequence of X st 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) ) ) ) & 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) ) ) ) holds
Sum p = Sum qlet a be
Function of
[:(Seg (n + 1)),(Seg m):],
X;
for p, q being FinSequence of X st 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) ) ) ) & 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) ) ) ) holds
Sum p = Sum qlet p,
q be
FinSequence of
X;
( 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) ) ) ) & 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) ) ) ) implies Sum p = Sum q )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) ) ) ) )
;
Sum p = Sum qA6:
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 H1(
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 for i being Nat st i in dom p0 holds
ex r being FinSequence of X st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . (i,j) ) )let i be
Nat;
( i in dom p0 implies ex r being FinSequence of X st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . (i,j) ) ) )assume A11:
i in dom p0
;
ex r being FinSequence of X st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . (i,j) ) )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;
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . (i,j) ) )thus
(
dom r = Seg m &
p0 . i = Sum r )
by A11, A12, FUNCT_1:47;
for j being Nat st j in dom r holds
r . j = a0 . (i,j)thus
for
j being
Nat st
j in dom r holds
r . j = a0 . (
i,
j)
verumproof
let j be
Nat;
( j in dom r implies r . j = a0 . (i,j) )
assume A13:
j in dom r
;
r . j = a0 . (i,j)
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;
verum
end; 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 = H1(
j) ) )
from FINSEQ_1:sch 2();
A15:
dom an = Seg m
by A14, FINSEQ_1:def 3;
then reconsider an =
an as
FinSequence of
X by FINSEQ_2:12;
A17:
Sum an = p . (n + 1)
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
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 for j being Nat st j in dom q0 holds
ex sn being FinSequence of X st
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . (i,j) ) )let j be
Nat;
( j in dom q0 implies ex sn being FinSequence of X st
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . (i,j) ) ) )assume A23:
j in dom q0
;
ex sn being FinSequence of X st
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . (i,j) ) )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;
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . (i,j) ) )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;
( q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . (i,j) ) )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;
for i being Nat st i in dom sn holds
sn . i = a0 . (i,j)thus
for
i being
Nat st
i in dom sn holds
sn . i = a0 . (
i,
j)
verumproof
let i be
Nat;
( i in dom sn implies sn . i = a0 . (i,j) )
assume A30:
i in dom sn
;
sn . i = a0 . (i,j)
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;
verum
end; end;
for
i being
Nat st 1
<= i &
i <= len q holds
q /. i = (q0 /. i) + (an /. i)
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;
verum end;
hence
S1[
n + 1]
;
verum
end;
now for m being Nat
for a being Function of [:(Seg 0),(Seg m):],X
for p, q being FinSequence of X st dom p = Seg 0 & ( 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 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) holds
Sum p = Sum qlet m be
Nat;
for a being Function of [:(Seg 0),(Seg m):],X
for p, q being FinSequence of X st dom p = Seg 0 & ( 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 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) holds
Sum p = Sum qlet a be
Function of
[:(Seg 0),(Seg m):],
X;
for p, q being FinSequence of X st dom p = Seg 0 & ( 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 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) holds
Sum p = Sum qlet p,
q be
FinSequence of
X;
( dom p = Seg 0 & ( 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 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) implies Sum p = Sum q )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) ) )
;
Sum p = Sum qA37:
p = <*> the
carrier of
X
by A32;
A38:
len q = len q
;
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;
verum end;
then A40:
S1[ 0 ]
;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A40, A1); verum