let A be non empty closed_interval Subset of REAL; for s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
for z being FinSequence of REAL
for g being Function of A,REAL
for t being Element of A st len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum z
let s be FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)); for z being FinSequence of REAL
for g being Function of A,REAL
for t being Element of A st len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum z
let z be FinSequence of REAL ; for g being Function of A,REAL
for t being Element of A st len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum z
let g be Function of A,REAL; for t being Element of A st len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum z
let t be Element of A; ( len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) implies g . t = Sum z )
assume A1:
( len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) )
; g . t = Sum z
defpred S1[ Nat] means for A being non empty closed_interval Subset of REAL
for s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
for z being FinSequence of REAL
for g being Function of A,REAL
for t being Element of A st len s = $1 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum z;
A2:
S1[ 0 ]
proof
let A be non
empty closed_interval Subset of
REAL;
for s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
for z being FinSequence of REAL
for g being Function of A,REAL
for t being Element of A st len s = 0 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum zlet s be
FinSequence of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A));
for z being FinSequence of REAL
for g being Function of A,REAL
for t being Element of A st len s = 0 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum zlet z be
FinSequence of
REAL ;
for g being Function of A,REAL
for t being Element of A st len s = 0 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum zlet g be
Function of
A,
REAL;
for t being Element of A st len s = 0 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum zlet t be
Element of
A;
( len s = 0 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) implies g . t = Sum z )
assume that A3:
len s = 0
and A4:
len s = len z
and A5:
g = Sum s
and
for
k being
Nat st
k in dom z holds
ex
sk being
Function of
A,
REAL st
(
sk = s . k &
z . k = sk . t )
;
g . t = Sum z
set V =
R_Normed_Algebra_of_BoundedFunctions the
carrier of
(ClstoCmp A);
set AV = the
carrier of
(ClstoCmp A);
B8:
Sum s =
0. (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
by A3, RLVECT_1:75
.=
the
carrier of
(ClstoCmp A) --> 0
by C0SP1:25
.=
A --> 0
by Lm1
;
z = <*> REAL
by A3, A4;
hence
g . t = Sum z
by B8, FUNCOP_1:7, A5, RVSUM_1:72;
verum
end;
A9:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A10:
S1[
n]
;
S1[n + 1]
let A be non
empty closed_interval Subset of
REAL;
for s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
for z being FinSequence of REAL
for g being Function of A,REAL
for t being Element of A st len s = n + 1 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum zlet s be
FinSequence of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A));
for z being FinSequence of REAL
for g being Function of A,REAL
for t being Element of A st len s = n + 1 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum zlet z be
FinSequence of
REAL ;
for g being Function of A,REAL
for t being Element of A st len s = n + 1 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum zlet g be
Function of
A,
REAL;
for t being Element of A st len s = n + 1 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) holds
g . t = Sum zlet t be
Element of
A;
( len s = n + 1 & len s = len z & g = Sum s & ( for k being Nat st k in dom z holds
ex sk being Function of A,REAL st
( sk = s . k & z . k = sk . t ) ) implies g . t = Sum z )
assume that A11:
len s = n + 1
and A12:
len s = len z
and A13:
g = Sum s
and A14:
for
k being
Nat st
k in dom z holds
ex
sk being
Function of
A,
REAL st
(
sk = s . k &
z . k = sk . t )
;
g . t = Sum z
set V =
R_Normed_Algebra_of_BoundedFunctions the
carrier of
(ClstoCmp A);
set AV = the
carrier of
(ClstoCmp A);
A15:
A = the
carrier of
(ClstoCmp A)
by Lm1;
set s0 =
s | n;
set z0 =
z | n;
A16:
for
k being
Nat st
k in dom (z | n) holds
ex
sk being
Function of
A,
REAL st
(
sk = (s | n) . k &
(z | n) . k = sk . t )
dom z = Seg (n + 1)
by A11, A12, FINSEQ_1:def 3;
then consider sk being
Function of
A,
REAL such that A19:
(
sk = s . (n + 1) &
z . (n + 1) = sk . t )
by A14, FINSEQ_1:4;
A20:
( 1
<= n + 1 &
n + 1
<= len z )
by A11, A12, NAT_1:11;
z = (z | n) ^ <*(z /. (n + 1))*>
by A11, A12, FINSEQ_5:21;
then B21:
z = (z | n) ^ <*(z . (n + 1))*>
by A20, FINSEQ_4:15;
Sum (s | n) is
Point of
(R_Normed_Algebra_of_BoundedFunctions A)
by Lm1;
then reconsider g1 =
Sum (s | n) as
Function of
A,
REAL by LM88;
dom s = Seg (n + 1)
by A11, FINSEQ_1:def 3;
then
s . (n + 1) in rng s
by FUNCT_1:3, FINSEQ_1:4;
then reconsider v =
s . (n + 1) as
Point of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ;
v is
Point of
(R_Normed_Algebra_of_BoundedFunctions A)
by Lm1;
then reconsider v1 =
v as
Function of
A,
REAL by LM88;
A23:
(
n = len (s | n) &
n = len (z | n) )
by A11, A12, FINSEQ_1:59, NAT_1:11;
then
s | n = s | (dom (s | n))
by FINSEQ_1:def 3;
then A24:
Sum s = (Sum (s | n)) + v
by A11, A23, RLVECT_1:38;
Sum s is
Point of
(R_Normed_Algebra_of_BoundedFunctions A)
by Lm1;
then reconsider g0 =
Sum s as
Function of
A,
REAL by LM88;
A25:
g0 . t = (g1 . t) + (sk . t)
by A19, A15, A24, C0SP1:29;
g1 . t = Sum (z | n)
by A10, A16, A23;
hence
g . t = Sum z
by A13, A25, B21, A19, RVSUM_1:74;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A9);
hence
g . t = Sum z
by A1; verum