let G be RealNormSpace-Sequence; :: thesis: ( ( for i being Element of dom G holds G . i is complete ) implies product G is complete )
assume A1:
for i being Element of dom G holds G . i is complete
; :: thesis: product G is complete
reconsider I = len G as Element of NAT ;
A2:
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #)
by Th6;
for seq being sequence of (product G) st seq is CCauchy holds
seq is convergent
proof
let seq be
sequence of
(product G);
:: thesis: ( seq is CCauchy implies seq is convergent )
assume A3:
seq is
CCauchy
;
:: thesis: seq is convergent
defpred S1[
Nat,
set ]
means ex
i being
Element of
dom G st
(
i = $1 & ex
seqi being
sequence of
(G . i) st
(
seqi is
convergent & $2
= lim seqi & ( for
m being
Element of
NAT ex
seqm being
Element of
product (carr G) st
(
seqm = seq . m &
seqi . m = seqm . i ) ) ) );
A11:
for
k being
Nat st
k in Seg I holds
ex
x being
set st
S1[
k,
x]
proof
let k be
Nat;
:: thesis: ( k in Seg I implies ex x being set st S1[k,x] )
assume
k in Seg I
;
:: thesis: ex x being set st S1[k,x]
then reconsider i =
k as
Element of
dom G by FINSEQ_1:def 3;
defpred S2[
Element of
NAT ,
Element of
(G . i)]
means ex
seqm being
Element of
product (carr G) st
(
seqm = seq . $1 & $2
= seqm . i );
A12:
for
x being
Element of
NAT ex
y being
Element of
(G . i) st
S2[
x,
y]
ex
f being
Function of
NAT ,the
carrier of
(G . i) st
for
x being
Element of
NAT holds
S2[
x,
f . x]
from FUNCT_2:sch 3(A12);
then consider seqi being
sequence of
(G . i) such that A15:
for
m being
Element of
NAT ex
seqm being
Element of
product (carr G) st
(
seqm = seq . m &
seqi . m = seqm . i )
;
A16:
G . i is
complete
by A1;
take x =
lim seqi;
:: thesis: S1[k,x]
then
seqi is
CCauchy
by RSSPACE3:10;
then
(
seqi is
convergent & ( for
m being
Element of
NAT ex
seqm being
Element of
product (carr G) st
(
seqm = seq . m &
seqi . m = seqm . i ) ) )
by A15, A16, LOPBAN_1:def 16;
hence
S1[
k,
x]
;
:: thesis: verum
end;
consider yy0 being
FinSequence such that A21:
(
dom yy0 = Seg I & ( for
j being
Nat st
j in Seg I holds
S1[
j,
yy0 . j] ) )
from FINSEQ_1:sch 1(A11);
yy0 is
Element of
product (carr G)
then reconsider y0 =
yy0 as
Element of
product (carr G) ;
reconsider x0 =
y0 as
Point of
(product G) by A2;
A24:
x0 = y0
;
hence
seq is
convergent
by A24, Th13;
:: thesis: verum
end;
hence
product G is complete
by LOPBAN_1:def 16; :: thesis: verum