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 Cauchy_sequence_by_Norm holds
seq is convergent

proof

let seq be sequence of (product G); :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
defpred S₁[ Nat, object ] 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 ) ) ) );
assume A3: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent
A4: for k being Nat st k in Seg I holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg I implies ex x being object st S₁[k,x] )
assume k in Seg I ; :: thesis: ex x being object st S₁[k,x]
then reconsider i = k as Element of dom G by FINSEQ_1:def 3;
defpred S₂[ Element of NAT , Element of (G . i)] means ex seqm being Element of product (carr G) st
( seqm = seq . $1 & $2 = seqm . i );
A5: for x being Element of NAT ex y being Element of (G . i) st S₂[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of (G . i) st S₂[x,y]
consider seqm being Element of product (carr G) such that
A6: seqm = seq . x by A2;
len G = len (carr G) by PRVECT_1:def 11;
then A7: dom G = dom (carr G) by FINSEQ_3:29;
take seqm . i ; :: thesis: ( seqm . i is Element of (G . i) & S₂[x,seqm . i] )
(carr G) . i = the carrier of (G . i) by PRVECT_1:def 11;
hence ( seqm . i is Element of (G . i) & S₂[x,seqm . i] ) by A6, A7, CARD_3:9; :: thesis: verum

end;

ex f being sequence of the carrier of (G . i) st
for x being Element of NAT holds S₂[x,f . x] from FUNCT_2:sch 3(A5);
then consider seqi being sequence of (G . i) such that
A8: for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ;
A9: for m being Nat ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i )

proof

let n be Nat; :: thesis: ex seqm being Element of product (carr G) st
( seqm = seq . n & seqi . n = seqm . i )
n in NAT by ORDINAL1:def 12;
hence ex seqm being Element of product (carr G) st
( seqm = seq . n & seqi . n = seqm . i ) by A8; :: thesis: verum

end;

take lim seqi ; :: thesis: S₁[k, lim seqi]

now :: thesis: for r1 being Real st r1 > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seqi . n) - (seqi . m)).|| < r1

let r1 be Real; :: thesis: ( r1 > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seqi . n) - (seqi . m)).|| < r1 )
assume A10: r1 > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seqi . n) - (seqi . m)).|| < r1
reconsider r = r1 as Element of REAL by XREAL_0:def 1;
consider k being Nat such that
A11: for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A3, A10, RSSPACE3:8;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((seqi . n) - (seqi . m)).|| < r1
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((seqi . n) - (seqi . m)).|| < r1 )
assume ( n >= k & m >= k ) ; :: thesis: ||.((seqi . n) - (seqi . m)).|| < r1
then A12: ||.((seq . n) - (seq . m)).|| < r by A11;
( ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) & ex seqn being Element of product (carr G) st
( seqn = seq . n & seqi . n = seqn . i ) ) by A9;
then ||.((seqi . n) - (seqi . m)).|| <= ||.((seq . n) - (seq . m)).|| by Th11;
hence ||.((seqi . n) - (seqi . m)).|| < r1 by A12, XXREAL_0:2; :: thesis: verum

end;

then A13: seqi is Cauchy_sequence_by_Norm by RSSPACE3:8;
G . i is complete by A1;
hence S₁[k, lim seqi] by A8, A13, LOPBAN_1:def 15; :: thesis: verum

end;

consider yy0 being FinSequence such that
A14: ( dom yy0 = Seg I & ( for j being Nat st j in Seg I holds
S₁[j,yy0 . j] ) ) from FINSEQ_1:sch 1(A4);
A15: len yy0 = I by A14, FINSEQ_1:def 3;
then A16: len yy0 = len (carr G) by PRVECT_1:def 11;

A17: now :: thesis: for i being object st i in dom (carr G) holds
yy0 . i in (carr G) . i

let i be object ; :: thesis: ( i in dom (carr G) implies yy0 . i in (carr G) . i )
assume i in dom (carr G) ; :: thesis: yy0 . i in (carr G) . i
then reconsider x = i as Element of dom (carr G) ;
reconsider x = x as Element of dom G by A15, A16, FINSEQ_3:29;
reconsider j = x as Element of NAT ;
j in dom G ;
then j in Seg I by FINSEQ_1:def 3;
then ex i0 being Element of dom G st
( i0 = j & ex seqi being sequence of (G . i0) st
( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i0 ) ) ) ) by A14;
then yy0 . x in the carrier of (G . x) ;
hence yy0 . i in (carr G) . i by PRVECT_1:def 11; :: thesis: verum

end;

( dom (carr G) = Seg (len (carr G)) & len G = len (carr G) ) by PRVECT_1:def 11, FINSEQ_1:def 3;
then reconsider y0 = yy0 as Element of product (carr G) by A14, A17, CARD_3:9;

A18: now :: thesis: for i being Element of dom G ex seqi being sequence of (G . i) st
( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) )

let i be Element of dom G; :: thesis: ex seqi being sequence of (G . i) st
( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) )
reconsider j = i as Element of NAT ;
i in dom G ;
then i in Seg I by FINSEQ_1:def 3;
then consider i0 being Element of dom G such that
A19: i0 = j and
A20: ex seqi being sequence of (G . i0) st
( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A14;
consider seqi being sequence of (G . i0) such that
A21: ( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A20;
reconsider seqi = seqi as sequence of (G . i) by A19;
take seqi = seqi; :: thesis: ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) )
thus ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st
( seqm = seq . m & seqi . m = seqm . i ) ) ) by A19, A21; :: thesis: verum

end;

reconsider x0 = y0 as Point of (product G) by A2;
x0 = y0 ;
hence seq is convergent by A18, Th13; :: thesis: verum

end;

hence product G is complete by LOPBAN_1:def 15; :: thesis: verum