defpred S1[ Nat] means for m being Nat
for a being Function of [:(Seg $1),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg $1 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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;
now for m being Nat
for a being Function of [:(Seg (n + 1)),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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):],REAL
for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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):],
REAL;
for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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
REAL ;
( dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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 A3:
dom p = Seg (n + 1)
and A4:
for
i being
Nat st
i in dom p holds
ex
r being
FinSequence of
REAL 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
and A6:
for
j being
Nat st
j in dom q holds
ex
s being
FinSequence of
REAL 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 qset a0 =
a | [:(Seg n),(Seg m):];
n <= n + 1
by NAT_1:11;
then
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
then
[:(Seg n),(Seg m):] c= [:(Seg (n + 1)),(Seg m):]
by ZFMISC_1:95;
then reconsider a0 =
a | [:(Seg n),(Seg m):] as
Function of
[:(Seg n),(Seg m):],
REAL by FUNCT_2:32;
deffunc H1(
Nat)
-> set =
a . [(n + 1),$1];
reconsider p0 =
p | (Seg n) as
FinSequence of
REAL by FINSEQ_1:18;
n + 1
in NAT
by ORDINAL1:def 12;
then
len p = n + 1
by A3, FINSEQ_1:def 3;
then A7:
n <= len p
by NAT_1:11;
then A8:
dom p0 = Seg n
by FINSEQ_1:17;
A9:
dom p0 = Seg n
by A7, FINSEQ_1:17;
A10:
now for i being Nat st i in dom p0 holds
ex r being FinSequence of REAL 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 REAL 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 REAL st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )consider r being
FinSequence of
REAL such that A12:
dom r = Seg m
and A13:
p . i = Sum r
and A14:
for
j being
Nat st
j in dom r holds
r . j = a . [i,j]
by A3, A4, A9, A11, 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
by A12;
( p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )thus
p0 . i = Sum r
by A11, A13, 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
n <= n + 1
by NAT_1:11;
then A15:
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
dom a = [:(Seg (n + 1)),(Seg m):]
by FUNCT_2:def 1;
then A16:
dom a0 =
[:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):]
by RELAT_1:61
.=
[:(Seg n),(Seg m):]
by A15, ZFMISC_1:101
;
let j be
Nat;
( j in dom r implies r . j = a0 . [i,j] )
assume A17:
j in dom r
;
r . j = a0 . [i,j]
A18:
[i,j] in [:(Seg n),(Seg m):]
by A9, A11, A12, A17, ZFMISC_1:87;
thus r . j =
a . [i,j]
by A14, A17
.=
a0 . [i,j]
by A18, A16, FUNCT_1:47
;
verum
end; end; reconsider m =
m as
Element of
NAT by ORDINAL1:def 12;
consider an being
FinSequence such that A19:
(
len an = m & ( for
j being
Nat st
j in dom an holds
an . j = H1(
j) ) )
from FINSEQ_1:sch 2();
A21:
dom an = Seg m
by A19, FINSEQ_1:def 3;
reconsider an =
an as
FinSequence of
REAL by A20, FINSEQ_2:12;
A22:
an is
Element of
m -tuples_on REAL
by A19, FINSEQ_2:92;
A23:
dom an = Seg m
by A19, FINSEQ_1:def 3;
A24:
Sum an = p . (n + 1)
reconsider q0 =
q - an as
FinSequence of
REAL ;
A29:
rng <:q,an:> c= [:(rng q),(rng an):]
by FUNCT_3:51;
dom diffreal = [:REAL,REAL:]
by FUNCT_2:def 1;
then A30:
[:(rng q),(rng an):] c= dom diffreal
by ZFMISC_1:96;
dom (diffreal .: (q,an)) =
dom (diffreal * <:q,an:>)
by FUNCOP_1:def 3
.=
dom <:q,an:>
by A30, A29, RELAT_1:27, XBOOLE_1:1
.=
(dom q) /\ (dom an)
by FUNCT_3:def 7
;
then A31:
dom q0 =
(dom q) /\ (dom an)
by RVSUM_1:def 6
.=
(Seg m) /\ (Seg m)
by A5, A19, FINSEQ_1:def 3
.=
Seg m
;
then
len q0 = m
by FINSEQ_1:def 3;
then A32:
q0 is
Element of
m -tuples_on REAL
by FINSEQ_2:92;
A33:
now for j being Nat st j in dom q0 holds
ex sn being FinSequence of REAL 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 REAL 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 A34:
j in dom q0
;
ex sn being FinSequence of REAL 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
REAL such that A35:
dom s = Seg (n + 1)
and A36:
q . j = Sum s
and A37:
for
i being
Nat st
i in dom s holds
s . i = a . [i,j]
by A5, A6, A31, A34;
s . (n + 1) = a . [(n + 1),j]
by A35, A37, FINSEQ_1:4;
then A38:
s . (n + 1) = an . j
by A19, A21, A31, A34;
reconsider sn =
s | (Seg n) as
FinSequence of
REAL 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] ) )
n + 1
in NAT
by ORDINAL1:def 12;
then A39:
len s = n + 1
by A35, FINSEQ_1:def 3;
then
n <= len s
by NAT_1:11;
hence A40:
dom sn = Seg n
by FINSEQ_1:17;
( q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) )
sn ^ <*(s . (n + 1))*> = s
by A39, FINSEQ_3:55;
then (q . j) - (an . j) =
((Sum sn) + (an . j)) - (an . j)
by A36, A38, RVSUM_1:74
.=
Sum sn
;
hence
q0 . j = Sum sn
by A34, VALUED_1:13;
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
n <= n + 1
by NAT_1:11;
then A41:
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
dom a = [:(Seg (n + 1)),(Seg m):]
by FUNCT_2:def 1;
then A42:
dom a0 =
[:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):]
by RELAT_1:61
.=
[:(Seg n),(Seg m):]
by A41, ZFMISC_1:101
;
let i be
Nat;
( i in dom sn implies sn . i = a0 . [i,j] )
assume A43:
i in dom sn
;
sn . i = a0 . [i,j]
A44:
[i,j] in [:(Seg n),(Seg m):]
by A31, A34, A40, A43, ZFMISC_1:87;
thus sn . i =
s . i
by A43, FUNCT_1:47
.=
a . [i,j]
by A35, A37, A40, A43, A41
.=
a0 . [i,j]
by A44, A42, FUNCT_1:47
;
verum
end; end;
len q = m
by A5, FINSEQ_1:def 3;
then
q is
Element of
m -tuples_on REAL
by FINSEQ_2:92;
then A45:
q0 + an = q
by A22, RVSUM_1:43;
n + 1
in NAT
by ORDINAL1:def 12;
then
len p = n + 1
by A3, FINSEQ_1:def 3;
then
p0 ^ <*(Sum an)*> = p
by A24, FINSEQ_3:55;
hence Sum p =
(Sum p0) + (Sum an)
by RVSUM_1:74
.=
(Sum q0) + (Sum an)
by A2, A10, A8, A31, A33
.=
Sum q
by A32, A22, A45, RVSUM_1:89
;
verum end;
hence
S1[
n + 1]
;
verum
end;
now for m being Nat
for a being Function of [:(Seg 0),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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):],REAL
for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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):],
REAL;
for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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
REAL ;
( dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL 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 REAL 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 A46:
dom p = Seg 0
and
for
i being
Nat st
i in dom p holds
ex
r being
FinSequence of
REAL 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 A47:
dom q = Seg m
and A48:
for
j being
Nat st
j in dom q holds
ex
s being
FinSequence of
REAL 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 qreconsider m =
m as
Element of
NAT by ORDINAL1:def 12;
then
q = (dom q) --> 0
by FUNCOP_1:11;
then A52:
q = m |-> 0
by A47, FINSEQ_2:def 2;
p = <*> REAL
by A46;
hence
Sum p = Sum q
by A52, RVSUM_1:72, RVSUM_1:81;
verum end;
then A53:
S1[ 0 ]
;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A53, A1); verum